Stefano Berardi

Gabriele Buriola

Peter Schuster

Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, 2024

2023

Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem.

[BibT_eX]

[DOI]

Adriano Barile

Luca Roversi

Proceedings of the 24th Italian Conference on Theoretical Computer Science, 2023

2019

An analysis of the Podelski-Rybalchenko termination theorem via bar recursion.

[BibT_eX]

[DOI]

Paulo Oliva

J. Log. Comput., 2019

Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2019

2018

Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs.

[BibT_eX]

[DOI]

Proceedings of the Coalgebraic Methods in Computer Science, 2018

2017

Ramsey's Theorem for Pairs and k Colors as a sub-Classical Principle of Arithmetic.

[BibT_eX]

[DOI]

J. Symb. Log., 2017

Non-monotonic Pre-fix Points and Learning.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2017

Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic.

[BibT_eX]

[DOI]

CoRR, 2017

Equivalence of inductive definitions and cyclic proofs under arithmetic.

[BibT_eX]

[DOI]

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System.

[BibT_eX]

[DOI]

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

2016

A Sound, Complete and Effective Second Order Game Semantics.

[BibT_eX]

[DOI]

CoRR, 2016

2015

An intuitionistic version of Ramsey's Theorem and its use in Program Termination.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2015

Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness.

[BibT_eX]

[DOI]

Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014

Knowledge Spaces and the Completeness of Learning Strategies.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2014

Proving termination with transition invariants of height omega.

[BibT_eX]

[DOI]

Paulo Oliva

CoRR, 2014

An intuitionistic version of Ramsey Theorem (italian version).

[BibT_eX]

[DOI]

CoRR, 2014

Ramsey Theorem as an Intuitionistic Property of Well Founded Relations.

[BibT_eX]

[DOI]

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

Proving termination of programs having transition invariants of height ω.

[BibT_eX]

[DOI]

Paulo Oliva

Proceedings of the 15th Italian Conference on Theoretical Computer Science, 2014

2013

Non-monotonic Pre-fixed Points and Learning.

[BibT_eX]

[DOI]

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

Preface.

[BibT_eX]

[DOI]

Steffen van Bakel

Ulrich Berger

Ann. Pure Appl. Log., 2013

Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the 19th International Conference on Types for Proofs and Programs, 2013

Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1.

[BibT_eX]

[DOI]

Federico Aschieri

Giovanni Birolo

Proceedings of the Computer Science Logic 2013 (CSL 2013), 2013

2012

Interactive Realizers: A New Approach to Program Extraction from Nonconstructive Proofs.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2012

Internal models of system F for decompilation.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2012

2011

Non-Commutative Infinitary Peano Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 2011

2010

Interactive Learning-Based Realizability for Heyting Arithmetic with EM1

[BibT_eX]

[DOI]

Federico Aschieri

Log. Methods Comput. Sci., 2010

Interactive Realizers and Monads

[BibT_eX]

[DOI]

CoRR, 2010

Games with 1-backtracking.

[BibT_eX]

[DOI]

Thierry Coquand

Susumu Hayashi

Ann. Pure Appl. Log., 2010

Internal Normalization, Compilation and Decompilation for System Fbh.

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming, 10th International Symposium, 2010

2009

Toward the interpretation of non-constructive reasoning as non-monotonic learning.

[BibT_eX]

[DOI]

Inf. Comput., 2009

Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1.

[BibT_eX]

[DOI]

Federico Aschieri

Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009

2008

Calculi, types and applications: Essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi Della Rocca.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2008

A sequent calculus for limit computable mathematics.

[BibT_eX]

[DOI]

Yoriyuki Yamagata

Ann. Pure Appl. Log., 2008

Preface.

[BibT_eX]

[DOI]

Steffen van Bakel

Ann. Pure Appl. Log., 2008

A Calculus of Realizers for EM1 Arithmetic (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

2007

Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves.

[BibT_eX]

[DOI]

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

Positive Arithmetic Without Exchange Is a Subclassical Logic.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 5th Asian Symposium, 2007

2006

Some intuitionistic equivalents of classical principles for degree 2 formulas.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2006

2005

Classical logic as limit completion.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2005

2004

Building continuous webbed models for system F.

[BibT_eX]

[DOI]

Chantal Berline

Theor. Comput. Sci., 2004

A generalization of a conservativity theorem for classical versus intuitionistic arithmetic.

[BibT_eX]

[DOI]

Math. Log. Q., 2004

Krivine's intuitionistic proof of classical completeness (for countable languages).

[BibT_eX]

[DOI]

Silvio Valentini

Ann. Pure Appl. Log., 2004

An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004

2003

A full continuous model of polymorphism.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2003

2002

BetaEta-Complete Models for System F.

[BibT_eX]

[DOI]

Chantal Berline

Math. Struct. Comput. Sci., 2002

2000

Type-Based Useless-Code Elimination for Functional Programs.

[BibT_eX]

[DOI]

Proceedings of the Semantics, 2000

1999

Intuitionistic Completeness for First Order Classical Logic.

[BibT_eX]

[DOI]

J. Symb. Log., 1999

Total Functionals and Well-Founded Strategies.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 4th International Conference, 1999

1998

Approximating Classical Theorems.

[BibT_eX]

[DOI]

Stefano Baratella

J. Log. Comput., 1998

On the Computational Content of the Axiom of Choice.

[BibT_eX]

[DOI]

Marc Bezem

Thierry Coquand

J. Symb. Log., 1998

1997

The Simply-Typed Theory of Beta-Conversion has no Maximum Extension.

[BibT_eX]

[DOI]

Inf. Comput., 1997

A parallel game semantics for Linear Logic.

[BibT_eX]

[DOI]

Stefano Baratella

Arch. Math. Log., 1997

Minimum Information Code in a Pure Functional Language with Data Types.

[BibT_eX]

[DOI]

Luca Boerio

Proceedings of the Typed Lambda Calculi and Applications, 1997

"Classical" Programming-with-Proofs in lambdaPASym: An Analysis of Non-confluence.

[BibT_eX]

[DOI]

Massimo Schivalocchi

Proceedings of the Theoretical Aspects of Computer Software, Third International Symposium, 1997

1996

A Constructive Valuation Semantics for Classical Logic.

[BibT_eX]

[DOI]

Notre Dame J. Formal Log., 1996

Pruning Simply Typed Lambda-Terms.

[BibT_eX]

[DOI]

J. Log. Comput., 1996

Proof-Irrelevance out of Exluded-Middle and Choice in the Calculus of Constructions.

[BibT_eX]

[DOI]

J. Funct. Program., 1996

A Symmetric Lambda Calculus for Classical Program Extraction.

[BibT_eX]

[DOI]

Inf. Comput., 1996

1995

A Strong Normalization Result for Classical Logic.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1995

A realization of the negative interpretation of the Axiom of Choice.

[BibT_eX]

[DOI]

Marc Bezem

Thierry Coquand

Proceedings of the Typed Lambda Calculi and Applications, 1995

Using Subtyping in Program Optimization.

[BibT_eX]

[DOI]

Luca Boerio

Proceedings of the Typed Lambda Calculi and Applications, 1995

1993

An Application of PER Models to Program Extraction.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 1993

Extracting Constructive Content from Classical Logic via Control-like Reductions.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 1993

1992

A Constructive Valuation Interpretation for Classical Logic and its Use in Witness Extraction.

[BibT_eX]

[DOI]

Proceedings of the CAAP '92, 1992

1991

Retractions on dI-domains as a model for Type:Type

[BibT_eX]

[DOI]

Inf. Comput., October, 1991

1988

Equalization of Finite Flowers.

[BibT_eX]

[DOI]