publicações selecionadas
-
artigo académico
- Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications. Journal of Logical and Algebraic Methods in Programming. 2023
-
documento
- Plotkin's call-by-value λ-calculus as a modal calculus. Journal of Logical and Algebraic Methods in Programming. 2022
- A coinductive approach to proof search through typed lambda-calculi. Annals of Pure and Applied Logic. 2021
- Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic. Leibniz International Proceedings in Informatics, LIPIcs. 2021
- 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
- Modal embeddings and calling paradigms. Leibniz International Proceedings in Informatics, LIPIcs. 2019
- A proof-theoretic study of bi-intuitionistic propositional sequent calculus. Journal of Logic and Computation. 2018
- Permutability in proof terms for intuitionistic sequent calculus with cuts. Leibniz International Proceedings in Informatics, LIPIcs. 2018
- Iluminando as mentes: da observação à disseminação dos fenómenos científicos 2016
- Computação: "The unreasonable effectiveness of mathematics in the computer/natural sciences" 2016
- Confluence for classical logic through the distinction between values and computations. Electronic Proceedings in Theoretical Computer Science. 2014
- A coinductive approach to proof search. Electronic Proceedings in Theoretical Computer Science. 2013
- Monadic translation of classical sequent calculus. Mathematical Structures in Computer Science. 2013
- A calculus of multiary sequent terms. ACM Transactions on Computational Logic. 2011
- Relating sequent calculi for bi-intuitionistic propositional logic. Electronic Proceedings in Theoretical Computer Science. 2011
- Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents. International Journal on Software Tools for Technology Transfer. 2009
- Structural proof theory as rewriting. International Journal on Software Tools for Technology Transfer. 2006
- Model checking embedded systems with PROMELA 2005
- Confluence and strong normalisation of the generalised multiary lambda-calculus. Annals of the New York Academy of Sciences. 2004
- Type-based termination of recursive definitions. Mathematical Structures in Computer Science. 2004
- Permutative conversions in intuitionistic multiary sequent calculi with cuts. International Journal on Software Tools for Technology Transfer. 2003
- Sequent calculi for the normal terms of the $\lambda\Pi$- and $\lambda\Pi\Sigma$-calculi. Electronic Notes in Theoretical Computer Science. 2000
- Permutability of proofs in intuitionistic sequent calculi. Theoretical Computer Science. 1999
- Proof search in constructive logics 1999
- Cut-elimination and a permutation-free sequent calculus for intuitionistic logic. Studia Logica. 1998
- Loop-free construction of counter-models for intuitionistic propositional logic 1995
- Cut formulae and logic programming 1994
-
livro