Gilles Dowek

Amélia Durbec

Proceedings of the Reversible Computation - 16th International Conference, 2024

From Rewrite Rules to Axioms in the $\lambda \varPi $-Calculus Modulo Theory.

[BibT_eX]

[DOI]

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

2023

Extensional proofs in a propositional logic modulo isomorphisms.

[BibT_eX]

[DOI]

Theor. Comput. Sci., October, 2023

A new connective in natural deduction, and its application to quantum computing.

[BibT_eX]

[DOI]

Theor. Comput. Sci., May, 2023

A modular construction of type theories.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2023

Permissive-Nominal Logic (journal version).

[BibT_eX]

[DOI]

CoRR, 2023

Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory.

[BibT_eX]

[DOI]

CoRR, 2023

Cut elimination for Zermelo set theory.

[BibT_eX]

[DOI]

Alexandre Miquel

CoRR, 2023

Relative normalization.

[BibT_eX]

[DOI]

Alexandre Miquel

CoRR, 2023

A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions.

[BibT_eX]

[DOI]

CoRR, 2023

Automatic Proof Checking and Proof Construction by Tactics.

[BibT_eX]

[DOI]

CoRR, 2023

The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors.

[BibT_eX]

[DOI]

CoRR, 2023

On Statman's Finite Completeness Theorem.

[BibT_eX]

[DOI]

Richard Statman

CoRR, 2023

A Unification Algorithm for Second-Order Linear Terms.

[BibT_eX]

[DOI]

CoRR, 2023

On the Definition of the Eta-long Normal Form in Type Systems of the Cube.

[BibT_eX]

[DOI]

Gérard Huet

CoRR, 2023

From proof theory to theories theory.

[BibT_eX]

[DOI]

CoRR, 2023

Preliminary investigations on induction over real numbers.

[BibT_eX]

[DOI]

CoRR, 2023

A constructive proof of Skolem theorem for constructive logic.

[BibT_eX]

[DOI]

CoRR, 2023

The Undecidability of Unification Modulo σ Alone.

[BibT_eX]

[DOI]

CoRR, 2023

Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View.

[BibT_eX]

[DOI]

CoRR, 2023

The physical Church-Turing thesis and non deterministic computation over the real numbers.

[BibT_eX]

[DOI]

CoRR, 2023

Logipedia: a multi-system encyclopedia of formal proofs.

[BibT_eX]

[DOI]

François Thiré

CoRR, 2023

Specifying programs with propositions and with congruences.

[BibT_eX]

[DOI]

CoRR, 2023

Simple Type Theory as a Clausal Theory.

[BibT_eX]

[DOI]

CoRR, 2023

The physical Church thesis and the sensitivity to initial conditions.

[BibT_eX]

[DOI]

CoRR, 2023

The principle of a finite density of information.

[BibT_eX]

[DOI]

CoRR, 2023

Complementation: a bridge between finite and infinite proofs.

[BibT_eX]

[DOI]

CoRR, 2023

Execution traces and reduction sequences.

[BibT_eX]

[DOI]

CoRR, 2023

Explanation: from ethics to logic.

[BibT_eX]

[DOI]

CoRR, 2023

Teaching G{ö}del's incompleteness theorems.

[BibT_eX]

[DOI]

CoRR, 2023

2022

Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs.

[BibT_eX]

[DOI]

Gaspard Férey

Jean-Pierre Jouannaud

Jiaxiang Liu

Math. Struct. Comput. Sci., August, 2022

Linear Lambda-Calculus is Linear.

[BibT_eX]

[DOI]

Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

From the Universality of Mathematical Truth to the Interoperability of Proof Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

Interacting Safely with an Unsafe Environment.

[BibT_eX]

[DOI]

Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2021

Some Axioms for Mathematics.

[BibT_eX]

[DOI]

Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction, 2021

2020

Theoretical Computer Science: Computational Complexity.

[BibT_eX]

[DOI]

Proceedings of the A Guided Tour of Artificial Intelligence Research: Volume III: Interfaces and Applications of Artificial Intelligence, 2020

Theoretical Computer Science: Computability, Decidability and Logic.

[BibT_eX]

[DOI]

Proceedings of the A Guided Tour of Artificial Intelligence Research: Volume III: Interfaces and Applications of Artificial Intelligence, 2020

2019

Towards Combining Model Checking and Proof Checking.

[BibT_eX]

[DOI]

Comput. J., 2019

Two linearities for quantum computing in the lambda calculus.

[BibT_eX]

[DOI]

Juan Pablo Rinaldi

Biosyst., 2019

Proof Normalisation in a Logic Identifying Isomorphic Propositions.

[BibT_eX]

[DOI]

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

2017

Lineal: A linear-algebraic Lambda-calculus.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2017

Rules and Derivations in an Elementary Logic Course.

[BibT_eX]

[DOI]

FLAP, 2017

Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems.

[BibT_eX]

[DOI]

Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, 2017

Typing Quantum Superpositions and Measurement.

[BibT_eX]

[DOI]

Proceedings of the Theory and Practice of Natural Computing - 6th International Conference, 2017

Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory.

[BibT_eX]

[DOI]

Proceedings of the 44th International Colloquium on Automata, Languages, and Programming, 2017

2016

Universality in two dimensions.

[BibT_eX]

[DOI]

Nachum Dershowitz

J. Log. Comput., 2016

Universality of Proofs (Dagstuhl Seminar 16421).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2016

SCTL: Towards Combining Model Checking and Proof Checking.

[BibT_eX]

[DOI]

CoRR, 2016

On the definition of the classical connectives and quantifiers.

[BibT_eX]

[DOI]

CoRR, 2016

Quantum superpositions and projective measurement in the lambda calculus.

[BibT_eX]

[DOI]

CoRR, 2016

2015

Deduction modulo theory.

[BibT_eX]

[DOI]

CoRR, 2015

Models and termination of proof-reduction in the $λ$$Π$-calculus modulo theory.

[BibT_eX]

[DOI]

CoRR, 2015

Free fall and cellular automata.

[BibT_eX]

[DOI]

Proceedings of the Eleventh International Workshop on Developments in Computational Models, 2015

Discrete Geodesics and Cellular Automata.

[BibT_eX]

[DOI]

Proceedings of the Theory and Practice of Natural Computing, 2015

Decidability, Introduction Rules and Automata.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

A Completion Method to Decide Reachability in Rewrite Systems.

[BibT_eX]

[DOI]

Guillaume Burel

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

2014

A Calculus for Automatic Verification of Petri Nets Based on Resolution and Dynamic Logics.

[BibT_eX]

[DOI]

Cláudia Nalon

Bruno Lopes

Edward Hermann Haeusler

Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

Yet Another Bijection Between Sequent Calculus and Natural Deduction.

[BibT_eX]

[DOI]

Cécilia Englander

Edward Hermann Haeusler

Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

Cut-elimination and the decidability of reachability in alternating pushdown systems.

[BibT_eX]

[DOI]

CoRR, 2014

2013

Causal graph dynamics.

[BibT_eX]

[DOI]

Inf. Comput., 2013

The probability of non-confluent systems.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 9th International Workshop on Developments in Computational Models, 2013

Real Numbers, Chaos, and the Principle of a Bounded Density of Information.

[BibT_eX]

[DOI]

Proceedings of the Computer Science - Theory and Applications, 2013

2012

Permissive-nominal logic: First-order logic over nominal terms and sets.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2012

PNL to HOL: From the logic of nominal sets to the logic of higher-order functions.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2012

Provably correct conflict prevention bands algorithms.

[BibT_eX]

[DOI]

Anthony Narkawicz

Sci. Comput. Program., 2012

A Simple Proof that Super-Consistency Implies Cut Elimination.

[BibT_eX]

[DOI]

Olivier Hermant

Notre Dame J. Formal Log., 2012

The physical Church thesis as an explanation of the Galileo thesis.

[BibT_eX]

[DOI]

Nat. Comput., 2012

Preface.

[BibT_eX]

[DOI]

Olivier Bournez

Nat. Comput., 2012

The Physical Church-Turing Thesis and the Principles of Quantum Theory.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2012

What Makes Alan Turing a Great Scientist? - Introduction to the Special Theme.

[BibT_eX]

[DOI]

Samson Abramsky

ERCIM News, 2012

Non determinism through type isomorphism

[BibT_eX]

[DOI]

Proceedings of the Proceedings Seventh Workshop on Logical and Semantic Frameworks, 2012

Around the Physical Church-Turing Thesis: Cellular Automata, Formal Languages, and the Principles of Quantum Theory.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2012

A Theory Independent Curry-De Bruijn-Howard Correspondence.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages, and Programming - 39th International Colloquium, 2012

Nominal Semantics for Predicate Logic: Algebras, Substitution, Quantifiers, and Limits.

[BibT_eX]

[DOI]

Proceedings of the 9th Italian Convention on Computational Logic, 2012

2011

Introduction to the Theory of Programming Languages.

[BibT_eX]

[DOI]

Jean-Jacques Lévy

Undergraduate Topics in Computer Science, Springer, ISBN: 978-0-85729-076-2, 2011

Proofs and Algorithms - An Introduction to Logic and Computability.

[BibT_eX]

[DOI]

Undergraduate Topics in Computer Science, Springer, ISBN: 978-0-85729-121-9, 2011

A formal library of set relations and its application to synchronous languages.

[BibT_eX]

[DOI]

Camilo Rocha

Theor. Comput. Sci., 2011

On the expressive power of schemes.

[BibT_eX]

[DOI]

Inf. Comput., 2011

From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions.

[BibT_eX]

[DOI]

Murdoch Gabbay

CoRR, 2011

2010

Preface.

[BibT_eX]

[DOI]

Alessandro Armando

Peter Baumgartner

J. Autom. Reason., 2010

Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques.

[BibT_eX]

[DOI]

Dominic P. Mulligan

Log. J. IGPL, 2010

Permissive-nominal logic.

[BibT_eX]

[DOI]

Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2010

How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project.

[BibT_eX]

Proceedings of the Second NASA Formal Methods Symposium, 2010

Polarized Resolution Modulo.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 2010

On the Completeness of Quantum Computation Models.

[BibT_eX]

[DOI]

Proceedings of the Programs, Proofs, Processes, 6th Conference on Computability in Europe, 2010

2009

Principles of Programming Languages.

[BibT_eX]

[DOI]

Undergraduate Topics in Computer Science, Springer, ISBN: 978-1-84882-032-6, 2009

On the convergence of reduction-based and model-based methods in proof theory.

[BibT_eX]

[DOI]

Log. J. IGPL, 2009

Rewriting Logic Semantics of a Plan Execution Language

[BibT_eX]

[DOI]

Camilo Rocha

Proceedings of the Proceedings Sixth Workshop on Structural Operational Semantics, 2009

Enumerating Proofs of Positive Formulae.

[BibT_eX]

[DOI]

Comput. J., 2009

How can we prove that a proof search method is not an instance of another?

[BibT_eX]

[DOI]

Guillaume Burel

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2009

2008

Linear-algebraic lambda-calculus: higher-order, encodings, and confluence..

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

2007

Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo.

[BibT_eX]

[DOI]

Denis Cousineau

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

2006

Eigenvariables, bracketing and the decidability of positive minimal predicate logic.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2006

Truth Values Algebras and Proof Normalization.

[BibT_eX]

[DOI]

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

Formal Analysis of the Operational Concept for the Small Aircraft Transportation System.

[BibT_eX]

[DOI]

Victor Carreño

Proceedings of the Rigorous Development of Complex Fault-Tolerant Systems [FP6 IST-511599 RODIN project], 2006

2005

Arithmetic as a Theory Modulo.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

What Do We Know When We Know That a Theory Is Consistent?.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2005

2004

A Computational Definition of the Notion of Vectorial Space.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications, 2004

Modeling and verification of an air traffic concept of operations.

[BibT_eX]

[DOI]

Victor Carreño

Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2004

2003

Formal verification of conflict detection algorithms.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2003

Proof normalization modulo.

[BibT_eX]

[DOI]

J. Symb. Log., 2003

Theorem Proving Modulo.

[BibT_eX]

[DOI]

J. Autom. Reason., 2003

Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic.

[BibT_eX]

[DOI]

Proceedings of the Mathematics, 2003

Confluence as a Cut Elimination Property.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

2002

What Is a Theory?

[BibT_eX]

[DOI]

Proceedings of the STACS 2002, 19th Annual Symposium on Theoretical Aspects of Computer Science, Antibes, 2002

Binding Logic: Proofs and Models.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2002

2001

HOL-λσ: an intentional first-order expression of higher-order logic.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2001

About Folding-Unfolding Cuts and Cuts Modulo.

[BibT_eX]

[DOI]

J. Log. Comput., 2001

The Stratified Foundations as a Theory Modulo.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

Higher-Order Unification and Matching.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000

Higher Order Unification via Explicit Substitutions.

[BibT_eX]

[DOI]

Inf. Comput., 2000

Axioms vs. Rewrite Rules: From Completeness to Cut Elimination.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2000

1999

Collections, sets and types.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 1999

HOL-<i>lambdasigma</i>: An Intentional First-Order Expression of Higher-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 10th International Conference, 1999

La part du calcul.

[BibT_eX]

[DOI]

, 1999

1998

Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction in Classical and Non-Classical Logics, 1998

1997

Proof Normalization for a First-Order Formulation of Higher-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 10th International Conference, 1997

1996

A Type-Free Formalization of Mathematics where Proofs are Objects.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, 1996

Unification via Explicit Substitutions: The Case of Higher-Order Patterns.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, 1996

1995

Lambda-calculus, Combinators and the Comprehension Scheme.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 1995

Higher-Order Unification via Explicit Substitutions (Extended Abstract)

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 1995

1994

Third Order Matching is Decidable.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1994

1993

The Undecidability of Pattern Matching in Calculi Where Primitive Recursive Functions are Representable.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1993

A Complete Proof Synthesis Method for the Cube of Type Systems.

[BibT_eX]

[DOI]

J. Log. Comput., 1993

The Undecidability of Typability in the Lambda-Pi-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 1993

1991

Démonstration Automatique dans le Calcul des Constructions. (Automated Theorem Proving in the Calculus of Constructions).

[BibT_eX]

[DOI]

PhD thesis, 1991

A Second-Order Pattern Matching Algorithm for the Cube of Typed Lambda-Calculi.

[BibT_eX]

[DOI]