publicações selecionadas
-
artigo de conferência
- Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic. Leibniz International Proceedings in Informatics, LIPIcs. 2021
- The call-by-value Lambda-Calculus with generalized applications. Leibniz International Proceedings in Informatics, LIPIcs. 2020
- Modal embeddings and calling paradigms. Leibniz International Proceedings in Informatics, LIPIcs. 2019
- Permutability in proof terms for intuitionistic sequent calculus with cuts. Leibniz International Proceedings in Informatics, LIPIcs. 2018
- Characterization of strong normalizability for a sequent lambda calculus with co-control 2017
- A note on strong normalization in classical natural deduction. Electronic Proceedings in Theoretical Computer Science. 2016
- Curry-Howard for sequent calculus at last!. Leibniz International Proceedings in Informatics, LIPIcs. 2015
- Confluence for classical logic through the distinction between values and computations. Electronic Proceedings in Theoretical Computer Science. 2014
- Sobre disjunções, confluências e o centro de gravidade da lógica filosófica 2014
- A coinductive approach to proof search. Electronic Proceedings in Theoretical Computer Science. 2013
- Towards a canonical classical natural deduction system. Computational Methods in Applied Sciences. 2010
- Characterising strongly normalising intuitionistic sequent terms. Computational Methods in Applied Sciences. 2008
- Completing herbelin's programme. Computational Methods in Applied Sciences. 2007
- Delayed substitutions. Computational Methods in Applied Sciences. 2007
- Refocusing generalised normalisation. Computational Methods in Applied Sciences. 2007
- Structural proof theory as rewriting. Computational Methods in Applied Sciences. 2006
- An isomorphism between a fragment of sequent calculus and an extension of natural deduction. Computational Methods in Applied Sciences. 2002
- Revisiting the correspondence between cut-elimination and normalisation 2000
-
artigo de revista
- A coinductive approach to proof search through typed lambda-calculi. Annals of Pure and Applied Logic. 2021
- The Russell-Prawitz embedding and the atomization of universal instantiation. Logic Journal of the IGPL. 2021
- A refined interpretation of intuitionistic logic by means of atomic polymorphism. Studia Logica. 2020
- Decidability of several concepts of finiteness for simple types. Fundamenta Informaticae. 2019
- Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search. Mathematical Structures in Computer Science. 2019
- The polarized λ-calculus. Electronic Notes in Theoretical Computer Science. 2017
- Monadic translation of classical sequent calculus. Mathematical Structures in Computer Science. 2013
- Towards a canonical classical natural deduction system. Annals of Pure and Applied Logic. 2013
- Characterising strongly normalising intuitionistic terms. Fundamenta Informaticae. 2012
- Turing e a normalização. Boletim da Sociedade Portuguesa de Matemática. 2012
- A calculus of multiary sequent terms. ACM Transactions on Computational Logic. 2011
- A note on preservation of strong normalisation in the lambda-calculus. Theoretical Computer Science. 2011
- The lambda-calculus and the unity of structural proof theory. Theory of Computing Systems. 2009
-
capítulo de livro
- Partial Proof Terms in the Study of Idealized Proof Search 2024
- Aplicações do processo diagonal 2019
- Confluence and strong normalisation of the generalised multiary lambda-calculus. Annals of the New York Academy of Sciences. 2004
- Permutative conversions in intuitionistic multiary sequent calculi with cuts. Computational Methods in Applied Sciences. 2003
-
documento