José Espírito Santo

Publication Activity (10 Years)

Years Active: 2000-2024
Publications (10 Years): 25

Top Topics

Theorem Proving

Sequent Calculus

Propositional Logic

Top Venues

J. Log. Algebraic Methods Program.

Publications

José Espírito Santo, Gilda Ferreira
How to avoid the commuting conversions of IPC. CoRR (2024)
José Espírito Santo, Delia Kesner, Loïc Peyrot
A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications. Log. Methods Comput. Sci. 20 (3) (2024)
José Espírito Santo, Ana Catarina Sousa
Partial Proof Terms in the Study of Idealized Proof Search. CICM (2024)
José Espírito Santo, Maria João Frade, Luís Pinto
Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications. J. Log. Algebraic Methods Program. 131 (2023)
José Espírito Santo, Filipa Mendes
The Logical Essence of Compiling With Continuations. CoRR (2023)
José Espírito Santo, Filipa Mendes
The Logical Essence of Compiling with Continuations. FSCD (2023)
José Espírito Santo, Delia Kesner, Loïc Peyrot
A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications. FoSSaCS (2022)
José Espírito Santo, Luís Pinto, Tarmo Uustalu
-calculus as a modal calculus. J. Log. Algebraic Methods Program. 127 (2022)
José Espírito Santo, Delia Kesner, Loïc Peyrot
A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications (Long Version). CoRR (2022)
José Espírito Santo, Gilda Ferreira
The Russell-Prawitz embedding and the atomization of universal instantiation. Log. J. IGPL 29 (5) (2021)
José Espírito Santo, Ralph Matthes, Luís Pinto
A coinductive approach to proof search through typed lambda-calculi. Ann. Pure Appl. Log. 172 (10) (2021)
José Espírito Santo, Ralph Matthes, Luís Pinto
Proof search for full intuitionistic propositional logic through a coinductive approach for polarized logic. CoRR (2020)
José Espírito Santo, Ralph Matthes, Luís Pinto
Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic. TYPES (2020)
José Espírito Santo
The Call-By-Value Lambda-Calculus with Generalized Applications. CSL (2020)
José Espírito Santo, Gilda Ferreira
A Refined Interpretation of Intuitionistic Logic by Means of Atomic Polymorphism. Stud Logica 108 (3) (2020)
José Espírito Santo, Ralph Matthes, Luís Pinto
Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search. Math. Struct. Comput. Sci. 29 (8) (2019)
José Espírito Santo, Luís Pinto, Tarmo Uustalu
Modal Embeddings and Calling Paradigms. FSCD (2019)
José Espírito Santo, Ralph Matthes, Luís Pinto
Decidability of Several Concepts of Finiteness for Simple Types. Fundam. Informaticae 170 (1-3) (2019)
José Espírito Santo, Silvia Ghilezan
Characterization of strong normalizability for a sequent lambda calculus with co-control. PPDP (2017)
José Espírito Santo
The Polarized λ-calculus. LSFA (2016)
José Espírito Santo, Maria João Frade, Luís Pinto
Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. TYPES (2016)
José Espírito Santo, Ralph Matthes, Luís Pinto
A Coinductive Approach to Proof Search through Typed Lambda-Calculi. CoRR (2016)
José Espírito Santo, Ralph Matthes, Luís Pinto
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search. CoRR (2016)
José Espírito Santo
A note on strong normalization in classical natural deduction. CL&C (2016)
José Espírito Santo
Curry-Howard for Sequent Calculus at Last!. TLCA (2015)
José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto
Confluence for classical logic through the distinction between values and computations. CL&C (2014)
José Espírito Santo, Ralph Matthes, Luís Pinto
A Coinductive Approach to Proof Search. FICS (2013)
José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto
Monadic translation of classical sequent calculus. Math. Struct. Comput. Sci. 23 (6) (2013)
José Espírito Santo
Towards a canonical classical natural deduction system. Ann. Pure Appl. Log. 164 (6) (2013)
José Espírito Santo, Jelena Ivetic, Silvia Likavec
Characterising Strongly Normalising Intuitionistic Terms. Fundam. Informaticae 121 (1-4) (2012)
José Espírito Santo, Luís Pinto
A calculus of multiary sequent terms. ACM Trans. Comput. Log. 12 (3) (2011)
José Espírito Santo
A note on preservation of strong normalisation in the λ-calculus. Theor. Comput. Sci. 412 (11) (2011)
José Espírito Santo
Towards a Canonical Classical Natural Deduction System. CSL (2010)
José Espírito Santo
-Calculus and the Unity of Structural Proof Theory. Theory Comput. Syst. 45 (4) (2009)
José Espírito Santo, Ralph Matthes, Luís Pinto
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi Log. Methods Comput. Sci. 5 (2) (2009)
José Espírito Santo, Ralph Matthes, Luís Pinto
Monadic Translation of Intuitionistic Sequent Calculus. TYPES (2008)
José Espírito Santo, Silvia Ghilezan, Jelena Ivetic
Characterising Strongly Normalising Intuitionistic Sequent Terms. TYPES (2007)
José Espírito Santo
Refocusing Generalised Normalisation. CiE (2007)
José Espírito Santo, Ralph Matthes, Luís Pinto
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi. TLCA (2007)
José Espírito Santo
Completing Herbelin's Programme. TLCA (2007)
José Espírito Santo
Delayed Substitutions. RTA (2007)
José Espírito Santo, Maria João Frade, Luís Pinto
Structural Proof Theory as Rewriting. RTA (2006)
José Espírito Santo, Luís Pinto
Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus. TYPES (2003)
José Espírito Santo, Luís Pinto
Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cuts. TLCA (2003)
José Espírito Santo
An Isomorphism between a Fragment of Sequent Calculus and an Extension of Natural Deduction. LPAR (2002)
José Espírito Santo
Revisiting the Correspondence between Cut Elimination and Normalisation. ICALP (2000)