José Espírito Santo

Delia Kesner

Loïc Peyrot

Log. Methods Comput. Sci., 2024

How to avoid the commuting conversions of IPC.

[BibT_eX]

[DOI]

Gilda Ferreira

CoRR, 2024

The logical essence of call-by-name CPS translations.

[BibT_eX]

[DOI]

Filipa Mendes

Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, 2024

Partial Proof Terms in the Study of Idealized Proof Search.

[BibT_eX]

[DOI]

Ana Catarina Sousa

Proceedings of the Intelligent Computer Mathematics - 17th International Conference, 2024

2023

Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications.

[BibT_eX]

[DOI]

Maria João Frade

J. Log. Algebraic Methods Program., February, 2023

The Logical Essence of Compiling with Continuations.

[BibT_eX]

[DOI]

Filipa Mendes

Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, 2023

2022

Plotkin's call-by-value <i>λ</i>-calculus as a modal calculus.

[BibT_eX]

[DOI]

Tarmo Uustalu

J. Log. Algebraic Methods Program., 2022

A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications (Long Version).

[BibT_eX]

[DOI]

Delia Kesner

Loïc Peyrot

CoRR, 2022

A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications.

[BibT_eX]

[DOI]

Delia Kesner

Loïc Peyrot

Proceedings of the Foundations of Software Science and Computation Structures, 2022

2021

The Russell-Prawitz embedding and the atomization of universal instantiation.

[BibT_eX]

[DOI]

Gilda Ferreira

Log. J. IGPL, 2021

A coinductive approach to proof search through typed lambda-calculi.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2021

2020

A Refined Interpretation of Intuitionistic Logic by Means of Atomic Polymorphism.

[BibT_eX]

[DOI]

Gilda Ferreira

Stud Logica, 2020

Proof search for full intuitionistic propositional logic through a coinductive approach for polarized logic.

[BibT_eX]

[DOI]

CoRR, 2020

Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Types for Proofs and Programs, 2020

The Call-By-Value Lambda-Calculus with Generalized Applications.

[BibT_eX]

[DOI]

Proceedings of the 28th EACSL Annual Conference on Computer Science Logic, 2020

2019

Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2019

Decidability of Several Concepts of Finiteness for Simple Types.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2019

Modal Embeddings and Calling Paradigms.

[BibT_eX]

[DOI]

Tarmo Uustalu

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

2017

Characterization of strong normalizability for a sequent lambda calculus with co-control.

[BibT_eX]

[DOI]

Silvia Ghilezan

Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09, 2017

2016

The Polarized λ-calculus.

[BibT_eX]

[DOI]

Proceedings of the 11th Workshop on Logical and Semantic Frameworks with Applications, 2016

A note on strong normalization in classical natural deduction.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Sixth International Workshop on Classical Logic and Computation, 2016

Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts.

[BibT_eX]

[DOI]

Maria João Frade

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

2015

Curry-Howard for Sequent Calculus at Last!.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

2014

Confluence for classical logic through the distinction between values and computations.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fifth International Workshop on Classical Logic and Computation, 2014

2013

Monadic translation of classical sequent calculus.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2013

A Coinductive Approach to Proof Search.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Workshop on Fixed Points in Computer Science, 2013

Towards a canonical classical natural deduction system.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2013

2012

Characterising Strongly Normalising Intuitionistic Terms.

[BibT_eX]

[DOI]

Jelena Ivetic

Silvia Likavec

Fundam. Informaticae, 2012

2011

A calculus of multiary sequent terms.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2011

A note on preservation of strong normalisation in the λ-calculus.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2011

2009

The <i>lambda</i>-Calculus and the Unity of Structural Proof Theory.

[BibT_eX]

[DOI]

Theory Comput. Syst., 2009

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2009

2008

Monadic Translation of Intuitionistic Sequent Calculus.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Conference, 2008

2007

Characterising Strongly Normalising Intuitionistic Sequent Terms.

[BibT_eX]

[DOI]

Silvia Ghilezan

Jelena Ivetic

Proceedings of the Types for Proofs and Programs, International Conference, 2007

Completing Herbelin's Programme.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 8th International Conference, 2007

Delayed Substitutions.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

Refocusing Generalised Normalisation.

[BibT_eX]

[DOI]

Proceedings of the Computation and Logic in the Real World, 2007

2006

Structural Proof Theory as Rewriting.

[BibT_eX]

[DOI]

Maria João Frade

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

2003

Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Workshop, 2003

Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cuts.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 6th International Conference, 2003

2002

An Isomorphism between a Fragment of Sequent Calculus and an Extension of Natural Deduction.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2002

2000

Revisiting the Correspondence between Cut Elimination and Normalisation.

[BibT_eX]

[DOI]