Cut Formulae and Logic Programming. - Luís Pinto 001 (ELP, 1993)

Uniform Proofs and Natural Deduction. - Roy Dyckhoff; Luís Pinto 001 (ICLP Workshop: Proof-Theoretical Extensions on Logic Programming, 1994)

Sequent Calculi for the Normal Terms of the - and - Calculi. - Luís Pinto 001; Roy Dyckhoff (Proof Search in Type-Theoretic Languages@CADE, 1998)

Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. - Roy Dyckhoff; Luís Pinto 001 (Stud Logica, 1998)

Permutability of Proofs in Intuitionistic Sequent Calculi. - Roy Dyckhoff; Luís Pinto 001 (Theor. Comput. Sci., 1999)

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)

Type-based termination of recursive definitions. - Gilles Barthe; Maria João Frade; Eduardo Giménez 001; Luís Pinto 001; Tarmo Uustalu (Math. Struct. Comput. Sci., 2004)

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

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

Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents. - Luís Pinto 001; Tarmo Uustalu (TABLEAUX, 2009)

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)

Relating Sequent Calculi for Bi-intuitionistic Propositional Logic - Luís Pinto 001; Tarmo Uustalu (CL&C, 2010)

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

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)

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 proof-theoretic study of bi-intuitionistic propositional sequent calculus. - Luís Pinto 001; Tarmo Uustalu (J. Log. Comput., 2018)

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)

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

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)

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)