A Second-Order Pattern Matching Algorithm for the Cube of Typed Lambda-Calculi. - Gilles Dowek (MFCS, 1991)

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

The Undecidability of Typability in the Lambda-Pi-Calculus. - Gilles Dowek (TLCA, 1993)

A Complete Proof Synthesis Method for the Cube of Type Systems. - Gilles Dowek (J. Log. Comput., 1993)

The Undecidability of Pattern Matching in Calculi Where Primitive Recursive Functions are Representable. - Gilles Dowek (Theor. Comput. Sci., 1993)

Third Order Matching is Decidable. - Gilles Dowek (Ann. Pure Appl. Log., 1994)

Higher-Order Unification via Explicit Substitutions (Extended Abstract) - Gilles Dowek; Thérèse Hardin; Claude Kirchner (LICS, 1995)

Lambda-calculus, Combinators and the Comprehension Scheme. - Gilles Dowek (TLCA, 1995)

Unification via Explicit Substitutions: The Case of Higher-Order Patterns. - Gilles Dowek; Thérèse Hardin; Claude Kirchner; Frank Pfenning (JICSLP, 1996)

A Type-Free Formalization of Mathematics where Proofs are Objects. - Gilles Dowek (TYPES, 1996)

Proof Normalization for a First-Order Formulation of Higher-Order Logic. - Gilles Dowek (TPHOLs, 1997)

Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory. - Gilles Dowek (FTP (LNCS Selection), 1998)

La part du calcul. - Gilles Dowek (1999)

HOL-lambdasigma: An Intentional First-Order Expression of Higher-Order Logic. - Gilles Dowek; Thérèse Hardin; Claude Kirchner (RTA, 1999)

Collections, sets and types. - Gilles Dowek (Math. Struct. Comput. Sci., 1999)

Axioms vs. Rewrite Rules: From Completeness to Cut Elimination. - Gilles Dowek (FroCoS, 2000)

Higher Order Unification via Explicit Substitutions. - Gilles Dowek; Thérèse Hardin; Claude Kirchner (Inf. Comput., 2000)

Higher-Order Unification and Matching. - Gilles Dowek (Handbook of Automated Reasoning, 2001)

The Stratified Foundations as a Theory Modulo. - Gilles Dowek (TLCA, 2001)

About Folding-Unfolding Cuts and Cuts Modulo. - Gilles Dowek (J. Log. Comput., 2001)

HOL-λσ: an intentional first-order expression of higher-order logic. - Gilles Dowek; Thérèse Hardin; Claude Kirchner (Math. Struct. Comput. Sci., 2001)

Binding Logic: Proofs and Models. - Gilles Dowek; Thérèse Hardin; Claude Kirchner (LPAR, 2002)

What Is a Theory? - Gilles Dowek (STACS, 2002)

Confluence as a Cut Elimination Property. - Gilles Dowek (RTA, 2003)

Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic. - Gilles Dowek; Ying Jiang 001 (Mathematics, Logic and Computation @ ICALP, 2003)

Theorem Proving Modulo. - Gilles Dowek; Thérèse Hardin; Claude Kirchner (J. Autom. Reason., 2003)

Proof normalization modulo. - Gilles Dowek; Benjamin Werner (J. Symb. Log., 2003)

Formal verification of conflict detection algorithms. - César A. Muñoz; Victor Carreño; Gilles Dowek; Ricky W. Butler (Int. J. Softw. Tools Technol. Transf., 2003)

Modeling and verification of an air traffic concept of operations. - César A. Muñoz; Gilles Dowek; Victor Carreño (ISSTA, 2004)

A Computational Definition of the Notion of Vectorial Space. - Pablo Arrighi; Gilles Dowek (WRLA, 2004)

What Do We Know When We Know That a Theory Is Consistent?. - Gilles Dowek (CADE, 2005)

Arithmetic as a Theory Modulo. - Gilles Dowek; Benjamin Werner (RTA, 2005)

Formal Analysis of the Operational Concept for the Small Aircraft Transportation System. - César A. Muñoz; Victor Carreño; Gilles Dowek (RODIN Book, 2006)

Truth Values Algebras and Proof Normalization. - Gilles Dowek (TYPES, 2006)

Eigenvariables, bracketing and the decidability of positive minimal predicate logic. - Gilles Dowek; Ying Jiang 001 (Theor. Comput. Sci., 2006)

Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. - Denis Cousineau 002; Gilles Dowek (TLCA, 2007)

Linear-algebraic lambda-calculus: higher-order, encodings, and confluence.. - Pablo Arrighi; Gilles Dowek (RTA, 2008)

How can we prove that a proof search method is not an instance of another? - Guillaume Burel; Gilles Dowek (LFMTP, 2009)

Enumerating Proofs of Positive Formulae. - Gilles Dowek; Ying Jiang 001 (Comput. J., 2009)

Rewriting Logic Semantics of a Plan Execution Language - Gilles Dowek; César A. Muñoz; Camilo Rocha (SOS, 2009)

On the convergence of reduction-based and model-based methods in proof theory. - Gilles Dowek (Log. J. IGPL, 2009)

Principles of Programming Languages. - Gilles Dowek (Springer, 2009)

On the Completeness of Quantum Computation Models. - Pablo Arrighi; Gilles Dowek (CiE, 2010)

Polarized Resolution Modulo. - Gilles Dowek (IFIP TCS, 2010)

How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project. - Ricky W. Butler; George Hagen; Jeffrey Maddalon; César A. Muñoz; Anthony Narkawicz; Gilles Dowek (NASA Formal Methods, 2010)

Permissive-nominal logic. - Gilles Dowek; Murdoch James Gabbay (PPDP, 2010)

Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques. - Gilles Dowek; Murdoch James Gabbay; Dominic P. Mulligan (Log. J. IGPL, 2010)

Preface. - Alessandro Armando; Peter Baumgartner 001; Gilles Dowek (J. Autom. Reason., 2010)

From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions. - Gilles Dowek; Murdoch Gabbay (CoRR, 2011)

On the expressive power of schemes. - Gilles Dowek; Ying Jiang 001 (Inf. Comput., 2011)

A formal library of set relations and its application to synchronous languages. - Camilo Rocha; César A. Muñoz; Gilles Dowek (Theor. Comput. Sci., 2011)

Proofs and Algorithms - An Introduction to Logic and Computability. - Gilles Dowek (Springer, 2011)

Introduction to the Theory of Programming Languages. - Gilles Dowek; Jean-Jacques Lévy (Springer, 2011)

Nominal Semantics for Predicate Logic: Algebras, Substitution, Quantifiers, and Limits. - Gilles Dowek; Murdoch James Gabbay (CILC, 2012)

A Theory Independent Curry-De Bruijn-Howard Correspondence. - Gilles Dowek (ICALP (2), 2012)

Around the Physical Church-Turing Thesis: Cellular Automata, Formal Languages, and the Principles of Quantum Theory. - Gilles Dowek (LATA, 2012)

Non determinism through type isomorphism - Alejandro Díaz-Caro; Gilles Dowek (LSFA, 2012)

What Makes Alan Turing a Great Scientist? - Introduction to the Special Theme. - Gilles Dowek; Samson Abramsky (ERCIM News, 2012)

The Physical Church-Turing Thesis and the Principles of Quantum Theory. - Pablo Arrighi; Gilles Dowek (Int. J. Found. Comput. Sci., 2012)

Preface. - Olivier Bournez; Gilles Dowek (Nat. Comput., 2012)

The physical Church thesis as an explanation of the Galileo thesis. - Gilles Dowek (Nat. Comput., 2012)

A Simple Proof that Super-Consistency Implies Cut Elimination. - Gilles Dowek; Olivier Hermant (Notre Dame J. Formal Log., 2012)

Provably correct conflict prevention bands algorithms. - Anthony Narkawicz; César A. Muñoz; Gilles Dowek (Sci. Comput. Program., 2012)

PNL to HOL: From the logic of nominal sets to the logic of higher-order functions. - Gilles Dowek; Murdoch James Gabbay (Theor. Comput. Sci., 2012)

Permissive-nominal logic: First-order logic over nominal terms and sets. - Gilles Dowek; Murdoch James Gabbay (ACM Trans. Comput. Log., 2012)

Real Numbers, Chaos, and the Principle of a Bounded Density of Information. - Gilles Dowek (CSR, 2013)

The probability of non-confluent systems. - Alejandro Díaz-Caro; Gilles Dowek (DCM, 2013)

Causal graph dynamics. - Pablo Arrighi; Gilles Dowek (Inf. Comput., 2013)

Cut-elimination and the decidability of reachability in alternating pushdown systems. - Gilles Dowek; Ying Jiang 001 (CoRR, 2014)

Yet Another Bijection Between Sequent Calculus and Natural Deduction. - Cécilia Englander; Gilles Dowek; Edward Hermann Haeusler (LSFA, 2014)

A Calculus for Automatic Verification of Petri Nets Based on Resolution and Dynamic Logics. - Cláudia Nalon; Bruno Lopes 001; Gilles Dowek; Edward Hermann Haeusler (LSFA, 2014)

A Completion Method to Decide Reachability in Rewrite Systems. - Guillaume Burel; Gilles Dowek; Ying Jiang 001 (FroCos, 2015)

Decidability, Introduction Rules and Automata. - Gilles Dowek; Ying Jiang 001 (LPAR, 2015)

Discrete Geodesics and Cellular Automata. - Pablo Arrighi; Gilles Dowek (TPNC, 2015)

Free fall and cellular automata. - Pablo Arrighi; Gilles Dowek (DCM, 2015)

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

Deduction modulo theory. - Gilles Dowek (CoRR, 2015)

Quantum superpositions and projective measurement in the lambda calculus. - Alejandro Díaz-Caro; Gilles Dowek (CoRR, 2016)

On the definition of the classical connectives and quantifiers. - Gilles Dowek (CoRR, 2016)

SCTL: Towards Combining Model Checking and Proof Checking. - Jian Liu; Gilles Dowek; Kailiang Ji; Ying Jiang 001 (CoRR, 2016)

Universality of Proofs (Dagstuhl Seminar 16421). - Gilles Dowek; Catherine Dubois; Brigitte Pientka; Florian Rabe 001 (Dagstuhl Reports, 2016)

Universality in two dimensions. - Nachum Dershowitz; Gilles Dowek (J. Log. Comput., 2016)

Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory. - Gilles Dowek (ICALP, 2017)

Typing Quantum Superpositions and Measurement. - Alejandro Díaz-Caro; Gilles Dowek (TPNC, 2017)

Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems. - Gilles Dowek (PxTP, 2017)

Rules and Derivations in an Elementary Logic Course. - Gilles Dowek (FLAP, 2017)

Lineal: A linear-algebraic Lambda-calculus. - Pablo Arrighi; Gilles Dowek (Log. Methods Comput. Sci., 2017)

Proof Normalisation in a Logic Identifying Isomorphic Propositions. - Alejandro Díaz-Caro; Gilles Dowek (FSCD, 2019)

Two linearities for quantum computing in the lambda calculus. - Alejandro Díaz-Caro; Gilles Dowek; Juan Pablo Rinaldi (Biosyst., 2019)

Towards Combining Model Checking and Proof Checking. - Ying Jiang 001; Jian Liu; Gilles Dowek; Kailiang Ji (Comput. J., 2019)

Theoretical Computer Science: Computability, Decidability and Logic. - Olivier Bournez; Gilles Dowek; Rémi Gilleron; Serge Grigorieff; Jean-Yves Marion; Simon Perdrix; Sophie Tison (A Guided Tour of Artificial Intelligence Research (3) (III), 2020)

Theoretical Computer Science: Computational Complexity. - Olivier Bournez; Gilles Dowek; Rémi Gilleron; Serge Grigorieff; Jean-Yves Marion; Simon Perdrix; Sophie Tison (A Guided Tour of Artificial Intelligence Research (3) (III), 2020)

Some Axioms for Mathematics. - Frédéric Blanqui; Gilles Dowek; Émilie Grienenberger; Gabriel Hondet; François Thiré (FSCD, 2021)

Interacting Safely with an Unsafe Environment. - Gilles Dowek (LFMTP, 2021)

From the Universality of Mathematical Truth to the Interoperability of Proof Systems. - Gilles Dowek (IJCAR, 2022)

Linear Lambda-Calculus is Linear. - Alejandro Díaz-Caro; Gilles Dowek (FSCD, 2022)

Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs. - Gilles Dowek; Gaspard Férey; Jean-Pierre Jouannaud; Jiaxiang Liu 001 (Math. Struct. Comput. Sci., 2022)

Teaching G{ö}del's incompleteness theorems. - Gilles Dowek (CoRR, 2023)

Explanation: from ethics to logic. - Gilles Dowek (CoRR, 2023)

Execution traces and reduction sequences. - Gilles Dowek (CoRR, 2023)

Complementation: a bridge between finite and infinite proofs. - Gilles Dowek; Ying Jiang 001 (CoRR, 2023)

The principle of a finite density of information. - Pablo Arrighi; Gilles Dowek (CoRR, 2023)

The physical Church thesis and the sensitivity to initial conditions. - Gilles Dowek (CoRR, 2023)

Simple Type Theory as a Clausal Theory. - Gilles Dowek (CoRR, 2023)

Specifying programs with propositions and with congruences. - Gilles Dowek (CoRR, 2023)

Logipedia: a multi-system encyclopedia of formal proofs. - Gilles Dowek; François Thiré (CoRR, 2023)

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

Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View. - Gilles Dowek (CoRR, 2023)

The Undecidability of Unification Modulo σ Alone. - Gilles Dowek (CoRR, 2023)

A constructive proof of Skolem theorem for constructive logic. - Gilles Dowek; Benjamin Werner (CoRR, 2023)

Preliminary investigations on induction over real numbers. - Gilles Dowek (CoRR, 2023)

From proof theory to theories theory. - Gilles Dowek (CoRR, 2023)

On the Definition of the Eta-long Normal Form in Type Systems of the Cube. - Gilles Dowek; Gérard Huet; Benjamin Werner (CoRR, 2023)

A Unification Algorithm for Second-Order Linear Terms. - Gilles Dowek (CoRR, 2023)

On Statman's Finite Completeness Theorem. - Richard Statman; Gilles Dowek (CoRR, 2023)

The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors. - Gilles Dowek (CoRR, 2023)

Automatic Proof Checking and Proof Construction by Tactics. - Gilles Dowek (CoRR, 2023)

A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions. - Gilles Dowek (CoRR, 2023)

Relative normalization. - Gilles Dowek; Alexandre Miquel (CoRR, 2023)

Cut elimination for Zermelo set theory. - Gilles Dowek; Alexandre Miquel (CoRR, 2023)

Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. - Ali Assaf 002; Guillaume Burel; Raphaël Cauderlier; David Delahaye; Gilles Dowek; Catherine Dubois; Frédéric Gilbert 002; Pierre Halmagrand; Olivier Hermant; Ronan Saillard (CoRR, 2023)

Permissive-Nominal Logic (journal version). - Gilles Dowek; Murdoch James Gabbay (CoRR, 2023)

A modular construction of type theories. - Frédéric Blanqui; Gilles Dowek; Émilie Grienenberger; Gabriel Hondet; François Thiré (Log. Methods Comput. Sci., 2023)

A new connective in natural deduction, and its application to quantum computing. - Alejandro Díaz-Caro; Gilles Dowek (Theor. Comput. Sci., 2023)

Extensional proofs in a propositional logic modulo isomorphisms. - Alejandro Díaz-Caro; Gilles Dowek (Theor. Comput. Sci., 2023)

From Rewrite Rules to Axioms in the $ lambda varPi $-Calculus Modulo Theory. - Valentin Blot; Gilles Dowek; Thomas Traversié; Théo Winterhalter (FoSSaCS (2), 2024)

A Toy Model Provably Featuring an Arrow of Time Without Past Hypothesis. - Pablo Arrighi; Gilles Dowek; Amélia Durbec (RC, 2024)

Reconstruction of SMT Proofs with Lambdapi. - Alessio Coltellacci; Stephan Merz; Gilles Dowek (SMT@CAV, 2024)

A Linear Proof Language for Second-Order Intuitionistic Linear Logic. - Alejandro Díaz-Caro; Gilles Dowek; Malena Ivnisky; Octavio Malherbe (WoLLIC, 2024)

From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory. - Valentin Blot; Gilles Dowek; Thomas Traversié; Théo Winterhalter (CoRR, 2024)

Space-time deterministic graph rewriting. - Pablo Arrighi; Marin Costes; Gilles Dowek; Luidnel Maignan (CoRR, 2024)

A linear linear lambda-calculus. - Alejandro Díaz-Caro; Gilles Dowek (Math. Struct. Comput. Sci., 2024)

A new introduction rule for disjunction. - Alejandro Díaz-Caro; Gilles Dowek (CoRR, 2025)