Publications

• Espírito Santo, J. Ferreira, G. How to avoid the commuting conversions of IPC, Theoretical Computer Science, 1033: 115101, 2025
• Espírito Santo, José Carlos, Diálogos com o futuro: comentários sobre Matemática Digital, in Estudos de História da Matemática, da Música e Militar, Ângela Cerdeira Lopes et al (orgs.), Maria Antónia Forjaz, Maria Elfrida Ralha (eds.), Braga, 2024, 362 pp, ISBN 978-989-8561-12-1. pdf file [In Portuguese]
• Espírito Santo,J., Kesner, D., Peyrot, L., A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications, Logical Methods in Computer Science, 20(3), 2024
• Espírito Santo, J., Sousa, A. C., Partial Proof Terms in the Study of Idealized Proof Search, Proc. of the 17^th International Conference on Intelligent Computer Mathematics (CICM), Lecture Notes in Computer Science, vol. 14960, pp 279--297, Springer, 2024
• Espírito Santo, J., Mendes, F., The essence of call-by-name CPS translations, Proc. of the 26^th International Symposium on Principles and Practice of Declarative Programming (PPDP), 11:1--11:12, ACM, 2024
• Espírito Santo, J., Frade, M. J., Pinto, L., Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications, Journal of Logical and Algebraic Methods in Programming, 131:100830, 2023
• Espírito Santo, J., Mendes, F., The logical essence of compiling with continuations, Proc. of 8^th International Conference on Formal Structures for Computation and Deduction (FSCD), LIPIcs, vol. 260, 19:1 - 19:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023
• Espírito Santo, J., Pinto, L., Uustalu, T., Plotkin's call-by-value λ-calculus as a modal calculus, Journal of Logical and Algebraic Methods in Programming, 127:100775, 2022
• Espírito Santo,J., Kesner, D., Peyrot, L., A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications, Proc. 25^th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Lecture Notes in Computer Science, vol. 13242, pp 285-304, Springer, 2022
• Espírito Santo, J., Matthes, R., Pinto, L, A coinductive approach to proof search through typed lambda calculi, Annals of Pure and Applied Logic, 172(10):103206, 2021
• Espírito Santo, J., Ferreira, G., The Russell-Prawitz embedding and the atomization of universal instantiation, Logical Journal of the IGPL, 29(5):823-858, 2021
• Espírito Santo, J., Ferreira, G., A Refined Interpretation of Intuitionistic Logic by Means of Atomic Polymorphism, Studia Logica, 108(3), 477 – 507, 2020.
• Espírito Santo, J., The call-by-value lambda-calculus with generalized applications. 28th Conference on Computer Science Logic (CSL) Barcelona, Spain, January 13-16, 2020. Dagstuhl - LIPIcs, 152 35:1-35:12, 2020.
• Espírito Santo, J., Matthes, R., Pinto, L, Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic, Proc. of the 26^th International Conference on Types for Proof and Programs (TYPES), LIPIcs, vol 188, 4:1—4:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020
• Espírito Santo, J., Matthes, R., Pinto, L, Decidability of several concepts of finiteness for simple types, Fundamenta Informaticae, 170(1-3) (2019) 111-138.
• Espírito Santo, J., Matthes, R., Pinto, L., Inhabitation in simply-typed lambda-calculus through a lambda-calculus for proof search, Mathematical Structures in Computer Science, 29(8) (2019) 1092-1124. (subsumes arXiv paper with same title)
• Espírito Santo, J., Pinto, L., Uustalu, T., Modal embeddings and calling paradigms. 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.
• 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 in proof terms for intuitionistic sequent calculus with cuts. Post-proceedings of Int. Conf. TYPES 2016, Novi Sad, Serbia, May, 23-26, 2016. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 97, 2018.
• Espírito Santo, J., The polarized lambda-calculus, Electronic Notes in Theoretical Computer Science 332 (2017), 149-168
• Espírito Santo, J., Ghilezan S., Characterization of strong normalizability for a sequent lambda calculus with co-control, Proccedings of the 19th International Symposium on Principles and Practice of Declarative Programming, ACM (2017), 163-174
• 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, A Coinductive Approach to Proof Search through Typed Lambda-Calculi, arXiv:1602.04382, 2016
• J. Espírito Santo, A note on strong normalization in classical natural deduction, Proceedings Sixth International Workshop on Classical Logic and Computation, CL&C 2016, EPTCS, vol. 213, pp. 41--51, 2016, url
• J. Espírito Santo, Curry-Howard for sequent calculus at last!, Proceedings of 13^th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), vol. 38 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015
• J. Espírito Santo, K. Nakazawa, R. Matthes, L. Pinto, Confluence for classical logic through the distinction between values and computations, Fifth International Workshop on Classical Logic and Computation (CL&C 2014), EPTCS vol. 164, pp. 63-77, 2014, pdf file
• J. Espírito Santo, R. Matthes, L. Pinto, A coinductive approach to proof search, Workshop on Fixed Points in Computer Science FICS 2013, EPTCS vol. 126, pp. 28-43, 2013, pdf file
• 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 Logic12(3):22, 2011 [Subsumes "Permutative conversions in intuitionistic multiary sequent calculus with cuts" (TLCA 2003)]
• J. Espírito Santo, Towards a canonical classical natural deduction system, in A. Dawar, H. Veith (Eds.), 19^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, Monadic translation of intuitionistic sequent calculus, 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
• 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 [Subsumes "Refocusing generalised normalisation"(CiE 2007) and "Completing Herbelin's programme" (TLCA 2007)] , pdf file
• J. Espírito Santo, Addenda to "Delayed Substitutions", Manuscript, July 2008, pdf file
• J. Espírito Santo, J. Ivetic, S. Likavec, Intersection type assignment systems for intuitionistic sequent calculus, 4^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, Characterising strongly normalising intuitionistic sequent terms, 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
• J. Espírito Santo, R. Matthes, L. Pinto, Continuation-passing-style and strong normalization for intuitionistic sequent calculi, S. Ronchi Della Rocca (ed.), Proceedings of 6^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, Completing Herbelin's programme, in S. Ronchi Della Rocca (ed.), Proceedings of 6^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, Delayed substitutions, in Franz Baader (ed.), Proceedings of 18^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, Refocusing generalised normalisation, 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
• J. Espírito Santo, M. J. Frade, L. Pinto, Structural proof theory as rewriting, in Proceedings of 17^th International Conference on Rewriting Techniques and Applications (RTA 2006), LNCS vol. 4098, Springer 2006, pdf file
• J. Espírito Santo, Unity in structural proof theory and structural extensions of the λ-calculus, Manuscript, July 2005, ps file
• J. Espírito Santo, L. Pinto, Confluence and strong normalization of the generalised multiary lambda-calculus, 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
• J. Espírito Santo, L. Pinto, Permutative conversions in intuitionistic multiary sequent calculus with cuts, in M. Hoffman (ed.), Proceedings of 6^th International Conference on Typed Lambda Calculi and Applications (TLCA 2003), LNCS vol. 2701, Springer, 2003, ps file
• J. Espírito Santo, An isomorphism between a fragment of sequent calculus and an extension of natural deduction, in M. Baaz, A. Voronkov (eds.), Proceedings of 9^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, Conservative extensions of the lambda-calculus for the computational interpretation of sequent calculus, Ph.D. thesis, Edinburgh 2002, available here as a technical report of LFCS, University of Edinburgh
• J. Espírito Santo, Revisiting the correspondence between cut-elimination and normalization, in Ugo Montanari, Jose D.P. Rolim, Emo Welzl (eds.), Proceedings of 27^th International Colloquium Automata, Languages, and Programming (ICALP 2000), Lecture Notes in Computer Science, vol. 1853, Springer 2000, ps file
• J. Espírito Santo, Chu e Galois: Polaridade, Conexão, Adjunção, MSc Thesis, Instituto Superior Técnico, Lisbon, April 1997 (in portuguese)