Papers

 

 

 

  • J. Espírito Santo, The polarized lambda-calculus, Proceedings of LSFA 2016, to appear
  • 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 13th 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, 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.), 19th 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, 4th 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 6th 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 6th 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 18th 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 17th 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 6th 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 9th 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 27th 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)