Proof Systems and Programming

Publications, chronologically

• 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, Barcelona, Spain, January 13-16, 2020. Dagstuhl - LIPIcs, 152 35:1-35:12, 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.
• Pinto, L., Uustalu, T., A proof-theoretic study of bi-intuitionistic propositional sequent calculus. Journal of Logic and Computation, 28(1): 165-202 (2018)
• 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’15), 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, J. Ivetic, S. Likavec, Characterising strongly normalising intuitionistic sequent terms, Fundamenta Informaticae, 121(1-4): 83-120, 2011 [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, 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
• L. Pinto, T. Uustalu, Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents, in M. Giese, A. Waaler (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods, 18th International Conference TABLEAUX 2009, Lecture Notes in Computer Science, volume 5607, pp. 295-309, Springer, 2009
• 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, 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, 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, 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, Springer, 2007, pdf file
• J. Espírito Santo, Delayed substitutions, in F. Baader (ed.), Proceedings of 18^th International Conference on Rewriting Techniques and Applications (RTA 2007), Lecture Notes in Computer Science, volume 4533, Springer, 2007, pdf file
• J. Espírito Santo, Refocusing generalised normalisation, in S. Barry Cooper, B. Loewe, A. 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, Springer 2007, pdf file
• J. Espírito Santo, M. J. Frade, and L. Pinto, Structural proof theory as rewriting, in F. Pfenning (ed), Proceedings of 17^th International Conference on Rewriting Techniques and Applications (RTA 2006), Lecture Notes in Computer Science 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
• O. Ribeiro, J.M. Fernandes and L. Pinto, Model checking embedded systems with PROMELA, 12th IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2005), IEEE Computer Society Press, 378-385, 2005 (v. RepositoriUM)
• G. Barthe, M.J. Frade, E. Giménez, L. Pinto and T. Uustalu, Type-based termination of recursive definitions, Mathematical Structures in Computer Science, 14:97-141,2004 (v. RepositoriUM)
• J. Espírito Santo and L. Pinto, Confluence and strong normalization of the generalised multiary lambda-calculus, in S. Berardi, M. Coppo, F. Damiani (eds.), Revised selected papers from the International Workshop TYPES 2003, Lecture Notes in Computer Science vol. 3085, Springer, 2004, ps file
• J. Espírito Santo and 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), Lecture Notes in Computer Science 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), 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, Edinburgh
• J. Espírito Santo, Revisiting the correspondence between cut-elimination and normalization, in U. Montanari, J. Rolim, E. 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
• R. Dyckhoff and L. Pinto, Permutability of proofs in intuitionistic sequent calculi, Theoretical Computer Science, 212:141-155, 1999 (v. ReposiroriUM)
• R. Dyckhoff and L. Pinto, Proof Search in Constructive Logics, in S. Barry Cooper and J. Truss (eds.), Sets and Proofs, London Mathematical Society LMS 258, 53-65, 1999 (v. RepositoriUM)
• R. Dyckhoff and L. Pinto, Cut-elimination and a permutation-free sequent calculus for intuitionistic logic, Studia Logica, 60:107-118, 1998 (v. RepositoriUM)
• L. Pinto and R. Dyckhoff, Sequent Calculi for the Normal Terms of the lambda-Pi- and lambda-Pi-Sigma Calculi, Electronic Notes in Theoretical Computer Science, 17, 1998 (v. RepositoriUM)
• L. Pinto, Proof Theoretic Investigations into Integrated Logic and Functional Programming, Ph.D. thesis, University of St Andrews, Scotland, 1996
• L. Pinto and R. Dyckhoff, Loop-Free Construction of Counter-Models for Intuitionistic Propositional Logic, in M. Behara, R. Fritsch and R. Lintz (eds.) Symposia Gaussiana, Conf. A, de Gruyter, 225-232, 1995 (v. RepositoriUM)
• L. Pinto and R. Dyckhoff, A Constructive Type System to Integrate Logic and Functional Programming, in D. Galmiche and L. Wallen (eds.) Proceedings of CADE--12 Workshop on Proof Search in Type-Theoretic Languages, INRIA LORRAINE -- CRIN, 70-81, 1994
• R. Dyckhoff and L. Pinto, Uniform Proofs and Natural Deductions, in D. Galmiche and L. Wallen (eds.) Proceedings of CADE--12 Workshop on Proof Search in Type-Theoretic Languages, INRIA LORRAINE -- CRIN, 17-23, 1994
• L. Pinto, Cut Formulae and Logic Programming, in R. Dyckhoff (ed.), Proceedings of 4^th International Workshop Extensions of Logic Programming (ELP 1993), Lecture Notes in Artificial Intelligence, vol. 798, 282-300, Springer, 1994 (v. RepositoriUM)