Publications

 

 

  • J. Espírito Santo, R. Matthes, L. Pinto, Decidability of several concepts of finiteness for simple types, to appear in Fundamenta Informaticae.
  • J. Espírito Santo,  L. Pinto, T. Uustalu Modal embeddings and calling paradigms, Proc. FSCD 2019, Dortmund, Germany, LIPIcs vol. 131, pp18:1-18:20, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. (doi link)
  • J. Espírito Santo, R. Matthes, L. Pinto, Inhabitation in simply-typed lambda-calculus through a lambda-calculus for proof search, Mathematical Structures in Computer Science, published online April 2018 (doi link)
  • L. Pinto, T. Uustalu, A proof-theoretic study of bi-intuitionistic propositional sequent calculus, Journal of Logic and Computation, 28(1):165-202,2018. (doi link)
  • J. Espírito Santo, M. J. Frade,  L. Pinto, Permutability in proof terms for intuitionistic sequent calculus with cuts, Post-proceedings of Int. Conf. TYPES 2016, Novi Sad, Serbia, LIPIcs vol. 97, pp10:1-10:27, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.  (doi link)
  • J. Espírito Santo, R. Matthes, K. Nakazawa, L. Pinto, Confluence for classical logic through the distinction between values and computations, in P. Oliva (Ed.), Proc. of  5th Workshop on Classical Logic and Computation (CL&C 2014), Viena, Austria, July 2014, Electron. Proc. in Theor. Comput. Sci.,  volume 164, pp. 63-77, 2014, Open Publishing Assoc. (doi link)
  • J. Espírito Santo, R. Matthes, K. Nakazawa, L. Pinto, Monadic translation of classical sequent calculus, Mathematical Structures in Computer Science, 23(6): 1111-1162, 2013, © Cambridge University Press
  • J. Espírito Santo, R. Matthes,  L. Pinto, A Coinductive Approach to Proof Search, in D. Baelde, A. Carayol (Eds.), Proc. of 9th Workshop on Fixed Points in Computer Science, FICS 2013, Torino, Italy, September 2013, Electron. Proc. in Theor. Comput. Sci., volume 126, pp. 28-43, Open Publishing Assoc. (doi link)
  • L. Pinto, T. Uustalu, Relating sequent calculi for bi-intuitionistic propositional logic, in S. van Bakel, S. Berardi, U. Berger (Eds.), Proc. of 3rd Workshop on Classical Logic and Computation, CL&C 2010, Brno, Czech Republic, August 2010, Electron. Proc. in Theor. Comput. Sci., volume 47, pp. 57-72, Open Publishing Assoc. (doi link)
  • J. Espírito Santo, L. Pinto, A calculus of multiary sequent terms, ACM Transactions on Computational Logic 12(3):22, 2011
  • 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, R. Matthes, L. Pinto,  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
  • 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
  • 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 6th International Conference on Typed Lambda Calculi and Applications (TLCA 2007), Lecture Notes in Computer Science, volume 4583, Springer, 2007
  • J. Espírito Santo, M. J. Frade,  L. Pinto, Structural proof theory as rewriting, in F. Pfenning (ed), Proceedings of 17th International Conference on Rewriting Techniques and Applications (RTA 2006), Lecture Notes in Computer Science vol. 4098, Springer, 2006      
  • 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, 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  
  • 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), Lecture Notes in Computer Science vol. 2701, Springer, 2003
  • R. Dyckhoff, L. Pinto, Permutability of proofs in intuitionistic sequent calculi, Theoretical Computer Science, 212:141-155, 1999 (v. RepositoriUM)
  • R. Dyckhoff, 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, L. Pinto, Cut-elimination and a permutation-free sequent calculus for intuitionistic logic, Studia Logica, 60:107-118, 1998 (v. RepositoriUM)
  • L. Pinto, 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, 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, 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, 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 4th International Workshop Extensions of Logic Programming (ELP 1993), Lecture Notes in Artificial Intelligence, vol. 798, 282-300, Springer, 1994 (v. RepositoriUM)