| Publication | Date of Publication | Type |
|---|
| Partial proof terms in the study of idealized proof search | 2024-12-04 | Paper |
| The logical essence of compiling with continuations | 2024-10-21 | Paper |
A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications Logical Methods in Computer Science | 2024-09-04 | Paper |
A faithful and quantitative notion of distant reduction for generalized applications Lecture Notes in Computer Science | 2024-01-23 | Paper |
Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications Journal of Logical and Algebraic Methods in Programming | 2023-02-03 | Paper |
Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus Journal of Logical and Algebraic Methods in Programming | 2022-05-25 | Paper |
| A note on strong normalization in classical natural deduction | 2021-12-07 | Paper |
A note on strong normalization in classical natural deduction (available as arXiv preprint) | 2021-12-07 | Paper |
The Russell-Prawitz embedding and the atomization of universal instantiation Logic Journal of the IGPL | 2021-12-03 | Paper |
A coinductive approach to proof search through typed lambda-calculi Annals of Pure and Applied Logic | 2021-09-30 | Paper |
| Confluence for classical logic through the distinction between values and computations | 2021-06-24 | Paper |
Confluence for classical logic through the distinction between values and computations (available as arXiv preprint) | 2021-06-24 | Paper |
| A coinductive approach to proof search | 2021-06-10 | Paper |
A coinductive approach to proof search (available as arXiv preprint) | 2021-06-10 | Paper |
| Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic | 2020-07-31 | Paper |
A refined interpretation of intuitionistic logic by means of atomic polymorphism Studia Logica | 2020-06-09 | Paper |
Decidability of several concepts of finiteness for simple types Fundamenta Informaticae | 2020-01-24 | Paper |
Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search Mathematical Structures in Computer Science | 2019-10-09 | Paper |
| The polarized \(\lambda\)-calculus | 2018-04-23 | Paper |
| Turing and normalization | 2018-01-09 | Paper |
| Curry-Howard for sequent calculus at last! | 2017-07-12 | Paper |
A Coinductive Approach to Proof Search through Typed Lambda-Calculi (available as arXiv preprint) | 2016-02-13 | Paper |
A calculus of multiary sequent terms ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Monadic translation of classical sequent calculus Mathematical Structures in Computer Science | 2014-04-16 | Paper |
Towards a canonical classical natural deduction system Annals of Pure and Applied Logic | 2013-04-15 | Paper |
Characterising strongly normalising intuitionistic terms Fundamenta Informaticae | 2013-01-24 | Paper |
A note on preservation of strong normalisation in the \(\lambda \)-calculus Theoretical Computer Science | 2011-03-14 | Paper |
Towards a Canonical Classical Natural Deduction System Computer Science Logic | 2010-09-03 | Paper |
The \(\lambda \)-calculus and the unity of structural proof theory Theory of Computing Systems | 2009-10-19 | Paper |
Monadic Translation of Intuitionistic Sequent Calculus Lecture Notes in Computer Science | 2009-07-02 | Paper |
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi Logical Methods in Computer Science | 2009-06-30 | Paper |
Completing Herbelin’s Programme Lecture Notes in Computer Science | 2009-03-10 | Paper |
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi Lecture Notes in Computer Science | 2009-03-10 | Paper |
Structural Proof Theory as Rewriting Lecture Notes in Computer Science | 2008-09-25 | Paper |
Characterising Strongly Normalising Intuitionistic Sequent Terms Lecture Notes in Computer Science | 2008-06-03 | Paper |
Delayed Substitutions Lecture Notes in Computer Science | 2008-01-02 | Paper |
Refocusing Generalised Normalisation Lecture Notes in Computer Science | 2007-11-13 | Paper |
Types for Proofs and Programs Lecture Notes in Computer Science | 2005-12-23 | Paper |
| scientific article; zbMATH DE number 2061717 (Why is no real title available?) | 2004-03-22 | Paper |
| scientific article; zbMATH DE number 1980937 (Why is no real title available?) | 2003-09-15 | Paper |
| scientific article; zbMATH DE number 1670856 (Why is no real title available?) | 2001-11-11 | Paper |
How to avoid the commuting conversions of IPC (available as arXiv preprint) | N/A | Paper |