Luís Pinto

Maria João Frade

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

2022

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

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2022

2021

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

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2021

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

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]

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

2018

A proof-theoretic study of bi-intuitionistic propositional sequent calculus.

[BibT_eX]

[DOI]

J. Log. Comput., 2018

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

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

2011

A calculus of multiary sequent terms.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2011

2010

Relating Sequent Calculi for Bi-intuitionistic Propositional Logic

[BibT_eX]

[DOI]

Proceedings of the Proceedings Third International Workshop on Classical Logic and Computation, 2010

2009

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2009

Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2009

2008

Monadic Translation of Intuitionistic Sequent Calculus.

[BibT_eX]

[DOI]

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

2006

Structural Proof Theory as Rewriting.

[BibT_eX]

[DOI]

Maria João Frade

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

2004

Type-based termination of recursive definitions.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2004

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

1999

Permutability of Proofs in Intuitionistic Sequent Calculi.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1999

1998

Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic.

[BibT_eX]

[DOI]

Stud Logica, 1998

Sequent Calculi for the Normal Terms of the - and - Calculi.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Proof Search in Type-Theoretic Languages (in conjunction with CADE-15 Conference), 1998

1994

Uniform Proofs and Natural Deduction.

[BibT_eX]

Proceedings of the ICLP 1994, 1994

1993

Cut Formulae and Logic Programming.

[BibT_eX]

[DOI]