José Espírito Santo

50 papers A* 1B 6C 5Journal 22Unranked 15

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