**Publications**

** **

** **

- Espírito Santo, J., Ferreira, G.,
, Studia Logica, 108(3), 477 – 507, 2020.*A Refined Interpretation of Intuitionistic Logic by Means of Atomic Polymorphism* - Espírito
Santo, J.,
*The*. 28th Conference on Computer Science Logic, Barcelona, Spain, January 13-16, 2020. Dagstuhl - LIPIcs, 152 35:1-35:12, 2020.*call-by-value lambda-calculus with generalized applications* - Espírito
Santo, J., Matthes, R., Pinto, L,
*Decidability*, Fundamenta Informaticae, 170(1-3) (2019) 111-138.*of several concepts of finiteness for simple types* - Espírito
Santo, J., Matthes, R., Pinto, L.,
*Inhabitation*, Mathematical Structures in Computer Science, 29(8) (2019) 1092-1124. (subsumes arXiv paper with same title)*in simply-typed lambda-calculus through a lambda-calculus for proof search* - Espírito
Santo, J., Pinto, L., Uustalu, T.,
. 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)., Dortmund, Germany, June, 24-30, 2019. Schloss Dagstuhl, LIPIcs 131 18:1–18:20, 2019.*Modal embeddings and calling paradigms* - Peter
Dybjer, José Espírito Santo, Luís Pinto (eds.), Post Proceedings of the 24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal, LIPIcs,
volume 130, Schloss Dagstuhl
- Leibniz-Zentrum fur Informatik, 2019 URL
- Espírito
Santo, J., Frade, M.J., Pinto, L.,
*Permutability*. Post-proceedings of Int. Conf. TYPES 2016, Novi Sad, Serbia, May, 23-26, 2016. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 97, 2018.*in proof terms for intuitionistic sequent calculus with cuts* - Espírito
Santo, J.,
*The*, Electronic Notes in Theoretical Computer Science 332 (2017), 149-168*polarized lambda-calculus* - Espírito
Santo, J., Ghilezan S.,
*Characterization*, Proccedings of the 19th International Symposium on Principles and Practice of Declarative Programming, ACM (2017), 163-174*of strong normalizability for a sequent lambda calculus with co-control* - J. Espírito Santo, R. Matthes, L. Pinto,
,*Inhabitation in simply-typed lambda-calculus through a lambda-calculus for proof search*arXiv:1604.02086, 2016 - J. Espírito Santo, R. Matthes, L. Pinto,
, arXiv:1602.04382, 2016*A Coinductive Approach to Proof Search through Typed Lambda-Calculi* - J. Espírito
Santo,
, Proceedings Sixth International Workshop on Classical Logic and Computation, CL&C 2016, EPTCS, vol. 213, pp. 41--51, 2016, url*A note on strong normalization in classical natural deduction* - J. Espírito
Santo,
, Proceedings of 13*Curry-Howard for sequent calculus at last!*^{th}International Conference on Typed Lambda Calculi and Applications (TLCA’15), vol. 38 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015 - J. Espírito
Santo, K. Nakazawa, R. Matthes,
L. Pinto,
, Fifth International Workshop on Classical Logic and Computation (CL&C 2014), EPTCS vol. 164, pp. 63-77, 2014, pdf file*Confluence for classical logic through the distinction between values and computations* - J. Espírito
Santo, R. Matthes, L. Pinto,
Workshop on Fixed Points in Computer Science FICS 2013, EPTCS vol. 126, pp. 28-43, 2013, pdf file*A coinductive approach to proof search*, - J. Espírito
Santo, K. Nakazawa, R. Matthes,
L. Pinto,
,*Monadic translation of classical sequent calculus**Mathematical Structures in Computer Science,*23(6): 1111-1162, 2013, © Cambridge University Press, pdf file - J. Espírito
Santo,
,*Towards a canonical classical natural deduction system**Annals of Pure and Applied Logic*, published online in 9 July 2012, pdf file [Subsumes CSL 2010 paper with the same title] - J.
Espírito Santo,
*Turing*,*e a normalização**Boletim da Sociedade Portuguesa de Matemática*, 67: 79-96, 2012, pdf file [In Portuguese] - J. Espírito
Santo, J. Ivetic, S. Likavec,
,*Characterising strongly normalising intuitionistic sequent terms**Fundamenta**Informaticae*, 121(1-4): 83-120, 2012 [Subsumes “*Characterising**strongly normalising intuitionistic sequent terms”*(TYPES’07) and “*Intersection type assignment systems for intuitionistic sequent calculus”*(ITRS’08)] - J. Espírito
Santo,
,*A note on preservation of strong normalisation in the lambda-calculus**Theoretical Computer Science*412(11): 1027-1032, 2011 [Journal version of “Addenda to ‘Delayed Substitutions’”, 2008] - J. Espírito
Santo, L. Pinto,
,*A calculus of multiary sequent terms**ACM Transactions on Computational Logic*12(3):22, 2011 [Subsumes “*Permutative**conversions in intuitionistic multiary sequent calculus with cuts’’*(TLCA 2003)] - J. Espírito
Santo,
, in A. Dawar, H. Veith (Eds.), 19*Towards a canonical classical natural deduction system*^{th}EACSL International Conference Computer Science Logic (CSL 2010), Lecture Notes in Computer Science, Springer, 2010, [Old version circulated with title “*A lambda-mu calculus with let-expressions*”], pdf file - J. Espírito
Santo, L. Pinto, R. Matthes,
, in S. Berardi, F. Damiani, U. de'Liguoro (Eds.), Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 2008, Revised Selected Papers, Lecture Notes in Computer Science, volume 5497, pp. 100-116, Springer, 2009, pdf file*Monadic translation of intuitionistic sequent calculus* - J. Espírito
Santo, R. Matthes, L. Pinto,
,*Continuation-passing-style and strong normalization for intuitionistic sequent calculi**Logical Methods in Computer Science*5(2:11), 2009 [Expanded and updated version of TLCA 2007 paper] , pdf file - J. Espírito
Santo,
,*The lambda-calculus and the unity of structural proof theory**Theory of Computing Systems*, 45:963-994, 2009*Refocusing generalised normalisation*”(CiE 2007) and “*Completing Herbelin’s programme*” (TLCA 2007)] , pdf file - J. Espírito
Santo,
, Manuscript, July 2008, pdf file*Addenda to “Delayed Substitutions”* - J. Espírito
Santo, J. Ivetic, S. Likavec,
, 4*Intersection type assignment systems for intuitionistic sequent calculus*^{th}Workshop on Intersection Types and Related Systems (ITRS’08), Turin , Italy, 25 March 2008, pdf file - J. Espírito
Santo, S. Ghilezan, J. Ivetic,
, M. Miculan, I. Scagnetto, F. Honsell (eds.), Revised selected papers from the International Workshop TYPES 2007, Lecture Notes in Computer Science, volume 4941, pp. 85-99, Springer, 2008, pdf file*Characterising strongly normalising intuitionistic sequent terms* - J. Espírito
Santo, R. Matthes, L. Pinto,
, S. Ronchi Della Rocca (ed.), Proceedings of 6*Continuation-passing-style and strong normalization for intuitionistic sequent calculi*^{th}International Conference on Typed Lambda Calculi and Applications (TLCA 2007), Lecture Notes in Computer Science, volume 4583, pp. 133-147, Springer, 2007, pdf file - J. Espírito
Santo,
, in S. Ronchi Della Rocca (ed.), Proceedings of 6*Completing Herbelin’s programme*^{th}International Conference on Typed Lambda Calculi and Applications (TLCA 2007), Lecture Notes in Computer Science, volume 4583, pp. 118-132, Springer, 2007, pdf file - J. Espírito
Santo,
, in Franz Baader (ed.), Proceedings of 18*Delayed substitutions*^{th}International Conference on Rewriting Techniques and Applications (RTA 2007), Lecture Notes in Computer Science, volume 4533, pp. 169-183, Springer, 2007, pdf file - J. Espírito
Santo,
, in S. Barry Cooper, Benedikt Loewe, Andrea Sorbi (eds.), Computation and Logic in the Real World, Third Conference on Computability in Europe (CiE 2007), Siena, Italy, June 2007, Proceedings, Lecture Notes in Computer Science, volume 4497, pp. 258-267, Springer 2007, pdf file*Refocusing generalised normalisation* - J. Espírito
Santo, M. J. Frade, L. Pinto,
, in Proceedings of 17*Structural proof theory as rewriting*^{th}International Conference on Rewriting Techniques and Applications (RTA 2006), LNCS vol. 4098, Springer 2006, pdf file - J. Espírito
Santo,
, Manuscript, July 2005, ps file*Unity in structural proof theory and structural extensions of the λ-calculus* - J. Espírito
Santo, L. Pinto,
, in Stefano Berardi, Mario Coppo, Ferruccio Damiani (eds.), Revised selected papers from the International Workshop TYPES 2003, Torino, Italy, April 30 – May 4 2003, LNCS vol. 3085, Springer 2004, ps file*Confluence and strong normalization of the generalised multiary lambda-calculus* - J. Espírito
Santo, L. Pinto,
*Permutative*, in M. Hoffman (ed.), Proceedings of 6*conversions in intuitionistic multiary sequent calculus with cuts*^{th}International Conference on Typed Lambda Calculi and Applications (TLCA 2003), LNCS vol. 2701, Springer, 2003, ps file - J. Espírito
Santo,
, in M. Baaz, A. Voronkov (eds.), Proceedings of 9*An isomorphism between a fragment of sequent calculus and an extension of natural deduction*^{th}International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2002), Tbilisi, Georgia, October 2002, Lecture Notes in Artificial Intelligence, vol. 2514, Springer 2002, ps file - J. Espírito
Santo,
, Ph.D. thesis, Edinburgh 2002, available here as a technical report of LFCS, University of Edinburgh*Conservative extensions of the lambda-calculus for the computational interpretation of sequent calculus* - J. Espírito
Santo,
, in Ugo Montanari, Jose D.P. Rolim, Emo Welzl (eds.), Proceedings of 27*Revisiting the correspondence between cut-elimination and normalization*^{th}International Colloquium Automata, Languages, and Programming (ICALP 2000), Lecture Notes in Computer Science, vol. 1853, Springer 2000, ps file - J. Espírito Santo,
, MSc Thesis, Instituto Superior Técnico, Lisbon, April 1997 (in portuguese)*Chu e Galois: Polaridade, Conexão, Adjunção*

* *

** **