Gilles Dowek

Orcid: 0000-0001-6253-935X

Affiliations:
  • INRIA, France


According to our database1, Gilles Dowek authored at least 126 papers between 1991 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory.
CoRR, 2024

2023
Extensional proofs in a propositional logic modulo isomorphisms.
Theor. Comput. Sci., October, 2023

A new connective in natural deduction, and its application to quantum computing.
Theor. Comput. Sci., May, 2023

A modular construction of type theories.
Log. Methods Comput. Sci., 2023

Permissive-Nominal Logic (journal version).
CoRR, 2023

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

Cut elimination for Zermelo set theory.
CoRR, 2023

Relative normalization.
CoRR, 2023

A linear proof language for second-order intuitionistic linear logic.
CoRR, 2023

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

Automatic Proof Checking and Proof Construction by Tactics.
CoRR, 2023

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

On Statman's Finite Completeness Theorem.
CoRR, 2023

A Unification Algorithm for Second-Order Linear Terms.
CoRR, 2023

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

A toy model provably featuring an arrow of time without past hypothesis.
CoRR, 2023

From proof theory to theories theory.
CoRR, 2023

Preliminary investigations on induction over real numbers.
CoRR, 2023

A constructive proof of Skolem theorem for constructive logic.
CoRR, 2023

The Undecidability of Unification Modulo σ Alone.
CoRR, 2023

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

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

Logipedia: a multi-system encyclopedia of formal proofs.
CoRR, 2023

Specifying programs with propositions and with congruences.
CoRR, 2023

Simple Type Theory as a Clausal Theory.
CoRR, 2023

The physical Church thesis and the sensitivity to initial conditions.
CoRR, 2023

The principle of a finite density of information.
CoRR, 2023

Complementation: a bridge between finite and infinite proofs.
CoRR, 2023

Execution traces and reduction sequences.
CoRR, 2023

Explanation: from ethics to logic.
CoRR, 2023

Teaching G{ö}del's incompleteness theorems.
CoRR, 2023

2022
Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs.
Math. Struct. Comput. Sci., August, 2022

Linear Lambda-Calculus is Linear.
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.
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021
Interacting Safely with an Unsafe Environment.
Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2021

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

2019
Towards Combining Model Checking and Proof Checking.
Comput. J., 2019

Two linearities for quantum computing in the lambda calculus.
Biosyst., 2019

Proof Normalisation in a Logic Identifying Isomorphic Propositions.
Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

2017
Lineal: A linear-algebraic Lambda-calculus.
Log. Methods Comput. Sci., 2017

Rules and Derivations in an Elementary Logic Course.
FLAP, 2017

Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems.
Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, 2017

Typing Quantum Superpositions and Measurement.
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.
Proceedings of the 44th International Colloquium on Automata, Languages, and Programming, 2017

2016
Universality in two dimensions.
J. Log. Comput., 2016

Universality of Proofs (Dagstuhl Seminar 16421).
Dagstuhl Reports, 2016

SCTL: Towards Combining Model Checking and Proof Checking.
CoRR, 2016

On the definition of the classical connectives and quantifiers.
CoRR, 2016

Quantum superpositions and projective measurement in the lambda calculus.
CoRR, 2016

2015
Deduction modulo theory.
CoRR, 2015

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

Free fall and cellular automata.
Proceedings of the Eleventh International Workshop on Developments in Computational Models, 2015

Discrete Geodesics and Cellular Automata.
Proceedings of the Theory and Practice of Natural Computing, 2015

Decidability, Introduction Rules and Automata.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

A Completion Method to Decide Reachability in Rewrite Systems.
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.
Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

Yet Another Bijection Between Sequent Calculus and Natural Deduction.
Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

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

2013
Causal graph dynamics.
Inf. Comput., 2013

The probability of non-confluent systems.
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.
Proceedings of the Computer Science - Theory and Applications, 2013

2012
Permissive-nominal logic: First-order logic over nominal terms and sets.
ACM Trans. Comput. Log., 2012

PNL to HOL: From the logic of nominal sets to the logic of higher-order functions.
Theor. Comput. Sci., 2012

Provably correct conflict prevention bands algorithms.
Sci. Comput. Program., 2012

A Simple Proof that Super-Consistency Implies Cut Elimination.
Notre Dame J. Formal Log., 2012

The physical Church thesis as an explanation of the Galileo thesis.
Nat. Comput., 2012

Preface.
Nat. Comput., 2012

The Physical Church-Turing Thesis and the Principles of Quantum Theory.
Int. J. Found. Comput. Sci., 2012

What Makes Alan Turing a Great Scientist? - Introduction to the Special Theme.
ERCIM News, 2012

Non determinism through type isomorphism
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.
Proceedings of the Language and Automata Theory and Applications, 2012

A Theory Independent Curry-De Bruijn-Howard Correspondence.
Proceedings of the Automata, Languages, and Programming - 39th International Colloquium, 2012

Nominal Semantics for Predicate Logic: Algebras, Substitution, Quantifiers, and Limits.
Proceedings of the 9th Italian Convention on Computational Logic, 2012

2011
Introduction to the Theory of Programming Languages.
Undergraduate Topics in Computer Science, Springer, ISBN: 978-0-85729-076-2, 2011

Proofs and Algorithms - An Introduction to Logic and Computability.
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.
Theor. Comput. Sci., 2011

On the expressive power of schemes.
Inf. Comput., 2011

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

2010
Preface.
J. Autom. Reason., 2010

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

Permissive-nominal logic.
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.
Proceedings of the Second NASA Formal Methods Symposium, 2010

Polarized Resolution Modulo.
Proceedings of the Theoretical Computer Science, 2010

On the Completeness of Quantum Computation Models.
Proceedings of the Programs, Proofs, Processes, 6th Conference on Computability in Europe, 2010

2009
Principles of Programming Languages.
Undergraduate Topics in Computer Science, Springer, ISBN: 978-1-84882-032-6, 2009

Rewriting Logic Semantics of a Plan Execution Language
Proceedings of the Proceedings Sixth Workshop on Structural Operational Semantics, 2009

Enumerating Proofs of Positive Formulae.
Comput. J., 2009

How can we prove that a proof search method is not an instance of another?
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..
Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

2007
On the Convergence of Reduction-based and Model-based Methods in Proof Theory.
Proceedings of the Second Workshop on Logical and Semantic Frameworks, with Applications, 2007

Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo.
Proceedings of the Typed Lambda Calculi and Applications, 8th International Conference, 2007

2006
Eigenvariables, bracketing and the decidability of positive minimal predicate logic.
Theor. Comput. Sci., 2006

Truth Values Algebras and Proof Normalization.
Proceedings of the Types for Proofs and Programs, International Workshop, 2006

Formal Analysis of the Operational Concept for the Small Aircraft Transportation System.
Proceedings of the Rigorous Development of Complex Fault-Tolerant Systems [FP6 IST-511599 RODIN project], 2006

2005
Arithmetic as a Theory Modulo.
Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

What Do We Know When We Know That a Theory Is Consistent?.
Proceedings of the Automated Deduction, 2005

2004
A Computational Definition of the Notion of Vectorial Space.
Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications, 2004

Modeling and verification of an air traffic concept of operations.
Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2004

2003
Formal verification of conflict detection algorithms.
Int. J. Softw. Tools Technol. Transf., 2003

Proof normalization modulo.
J. Symb. Log., 2003

Theorem Proving Modulo.
J. Autom. Reason., 2003

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

Confluence as a Cut Elimination Property.
Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

2002
What Is a Theory?
Proceedings of the STACS 2002, 19th Annual Symposium on Theoretical Aspects of Computer Science, Antibes, 2002

Binding Logic: Proofs and Models.
Proceedings of the Logic for Programming, 2002

2001
HOL-λσ: an intentional first-order expression of higher-order logic.
Math. Struct. Comput. Sci., 2001

About Folding-Unfolding Cuts and Cuts Modulo.
J. Log. Comput., 2001

The Stratified Foundations as a Theory Modulo.
Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

Higher-Order Unification and Matching.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000
Higher Order Unification via Explicit Substitutions.
Inf. Comput., 2000

Axioms vs. Rewrite Rules: From Completeness to Cut Elimination.
Proceedings of the Frontiers of Combining Systems, 2000

1999
Collections, sets and types.
Math. Struct. Comput. Sci., 1999

HOL-<i>lambdasigma</i>: An Intentional First-Order Expression of Higher-Order Logic.
Proceedings of the Rewriting Techniques and Applications, 10th International Conference, 1999

La part du calcul.
, 1999

1998
Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory.
Proceedings of the Automated Deduction in Classical and Non-Classical Logics, 1998

1997
Proof Normalization for a First-Order Formulation of Higher-Order Logic.
Proceedings of the Theorem Proving in Higher Order Logics, 10th International Conference, 1997

1996
A Type-Free Formalization of Mathematics where Proofs are Objects.
Proceedings of the Types for Proofs and Programs, 1996

Unification via Explicit Substitutions: The Case of Higher-Order Patterns.
Proceedings of the Logic Programming, 1996

1995
Lambda-calculus, Combinators and the Comprehension Scheme.
Proceedings of the Typed Lambda Calculi and Applications, 1995

Higher-Order Unification via Explicit Substitutions (Extended Abstract)
Proceedings of the Proceedings, 1995

1994
Third Order Matching is Decidable.
Ann. Pure Appl. Log., 1994

1993
The Undecidability of Pattern Matching in Calculi Where Primitive Recursive Functions are Representable.
Theor. Comput. Sci., 1993

A Complete Proof Synthesis Method for the Cube of Type Systems.
J. Log. Comput., 1993

The Undecidability of Typability in the Lambda-Pi-Calculus.
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).
PhD thesis, 1991

A Second-Order Pattern Matching Algorithm for the Cube of Typed Lambda-Calculi.
Proceedings of the Mathematical Foundations of Computer Science 1991, 1991


  Loading...