Revisiting the Correspondence between Cut Elimination and Normalisation. - José Espírito Santo (ICALP, 2000)

An Isomorphism between a Fragment of Sequent Calculus and an Extension of Natural Deduction. - José Espírito Santo (LPAR, 2002)

Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cuts. - José Espírito Santo; Luís Pinto 001 (TLCA, 2003)

Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus. - José Espírito Santo; Luís Pinto 001 (TYPES, 2003)

Structural Proof Theory as Rewriting. - José Espírito Santo; Maria João Frade; Luís Pinto 001 (RTA, 2006)

Refocusing Generalised Normalisation. - José Espírito Santo (CiE, 2007)

Delayed Substitutions. - José Espírito Santo (RTA, 2007)

Completing Herbelin's Programme. - José Espírito Santo (TLCA, 2007)

Characterising Strongly Normalising Intuitionistic Sequent Terms. - José Espírito Santo; Silvia Ghilezan; Jelena Ivetic (TYPES, 2007)

Monadic Translation of Intuitionistic Sequent Calculus. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (TYPES, 2008)

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (Log. Methods Comput. Sci., 2009)

The lambda-Calculus and the Unity of Structural Proof Theory. - José Espírito Santo (Theory Comput. Syst., 2009)

A note on preservation of strong normalisation in the λ-calculus. - José Espírito Santo (Theor. Comput. Sci., 2011)

A calculus of multiary sequent terms. - José Espírito Santo; Luís Pinto 001 (ACM Trans. Comput. Log., 2011)

Characterising Strongly Normalising Intuitionistic Terms. - José Espírito Santo; Jelena Ivetic; Silvia Likavec (Fundam. Informaticae, 2012)

Towards a canonical classical natural deduction system. - José Espírito Santo (Ann. Pure Appl. Log., 2013)

A Coinductive Approach to Proof Search. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (FICS, 2013)

Monadic translation of classical sequent calculus. - José Espírito Santo; Ralph Matthes; Koji Nakazawa; Luís Pinto 001 (Math. Struct. Comput. Sci., 2013)

Confluence for classical logic through the distinction between values and computations. - José Espírito Santo; Ralph Matthes; Koji Nakazawa; Luís Pinto 001 (CL&C, 2014)

Curry-Howard for Sequent Calculus at Last!. - José Espírito Santo (TLCA, 2015)

Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. - José Espírito Santo; Maria João Frade; Luís Pinto 001 (TYPES, 2016)

A note on strong normalization in classical natural deduction. - José Espírito Santo (CL&C, 2016)

The Polarized λ-calculus. - José Espírito Santo (LSFA, 2016)

Characterization of strong normalizability for a sequent lambda calculus with co-control. - José Espírito Santo; Silvia Ghilezan (PPDP, 2017)

Modal Embeddings and Calling Paradigms. - José Espírito Santo; Luís Pinto 001; Tarmo Uustalu (FSCD, 2019)

Decidability of Several Concepts of Finiteness for Simple Types. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (Fundam. Informaticae, 2019)

Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (Math. Struct. Comput. Sci., 2019)

The Call-By-Value Lambda-Calculus with Generalized Applications. - José Espírito Santo (CSL, 2020)

Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (TYPES, 2020)

Proof search for full intuitionistic propositional logic through a coinductive approach for polarized logic. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (CoRR, 2020)

A Refined Interpretation of Intuitionistic Logic by Means of Atomic Polymorphism. - José Espírito Santo; Gilda Ferreira (Stud Logica, 2020)

A coinductive approach to proof search through typed lambda-calculi. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (Ann. Pure Appl. Log., 2021)

The Russell-Prawitz embedding and the atomization of universal instantiation. - José Espírito Santo; Gilda Ferreira (Log. J. IGPL, 2021)

A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications. - José Espírito Santo; Delia Kesner; Loïc Peyrot (FoSSaCS, 2022)

A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications (Long Version). - José Espírito Santo; Delia Kesner; Loïc Peyrot (CoRR, 2022)

Plotkin's call-by-value λ-calculus as a modal calculus. - José Espírito Santo; Luís Pinto 001; Tarmo Uustalu (J. Log. Algebraic Methods Program., 2022)

The Logical Essence of Compiling with Continuations. - José Espírito Santo; Filipa Mendes (FSCD, 2023)

Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications. - José Espírito Santo; Maria João Frade; Luís Pinto 001 (J. Log. Algebraic Methods Program., 2023)

Partial Proof Terms in the Study of Idealized Proof Search. - José Espírito Santo; Ana Catarina Sousa (CICM, 2024)

The logical essence of call-by-name CPS translations. - José Espírito Santo; Filipa Mendes (PPDP, 2024)

A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications. - José Espírito Santo; Delia Kesner; Loïc Peyrot (Log. Methods Comput. Sci., 2024)

Proof Search in Classical Propositional Logic with Partial Proof Terms. - José Espírito Santo; Ana Catarina Sousa (WoLLIC, 2025)

How to avoid the commuting conversions of IPC. - José Espírito Santo; Gilda Ferreira (Theor. Comput. Sci., 2025)