Gilles Dowek

ORCID

Publication Activity (10 Years)

Years Active: 1991-2024
Publications (10 Years): 85

Top Venues

Publications

Pablo Arrighi, Marin Costes, Gilles Dowek, Luidnel Maignan
Space-time deterministic graph rewriting. CoRR (2024)
Alessio Coltellacci, Stephan Merz, Gilles Dowek
Reconstruction of SMT Proofs with Lambdapi. SMT@CAV (2024)
Pablo Arrighi, Gilles Dowek, Amélia Durbec
A Toy Model Provably Featuring an Arrow of Time Without Past Hypothesis. RC (2024)
Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky, Octavio Malherbe
A Linear Proof Language for Second-Order Intuitionistic Linear Logic. WoLLIC (2024)
Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter
From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory. CoRR (2024)
Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter
From Rewrite Rules to Axioms in the $\lambda \varPi $-Calculus Modulo Theory. FoSSaCS (2) (2024)
Gilles Dowek
Axioms vs. rewrite rules: from completeness to cut elimination. CoRR (2023)
Gilles Dowek, Murdoch James Gabbay, Dominic P. Mulligan
Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques. CoRR (2023)
Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky, Octavio Malherbe
A linear proof language for second-order intuitionistic linear logic. CoRR (2023)
Alejandro Díaz-Caro, Gilles Dowek
A new connective in natural deduction, and its application to quantum computing. Theor. Comput. Sci. 957 (2023)
Alejandro Díaz-Caro, Gilles Dowek
Extensional proofs in a propositional logic modulo isomorphisms. Theor. Comput. Sci. 977 (2023)
Gilles Dowek, Benjamin Werner
A constructive proof of Skolem theorem for constructive logic. CoRR (2023)
Gilles Dowek
Truth values algebras and proof normalization. CoRR (2023)
Gilles Dowek
What is a Theory ? CoRR (2023)
Gilles Dowek
The Undecidability of Typability in the Lambda-Pi-Calculus. CoRR (2023)
Gilles Dowek
Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory. CoRR (2023)
Gilles Dowek, Murdoch James Gabbay
Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits. CoRR (2023)
Gilles Dowek, Thérèse Hardin, Claude Kirchner
Binding Logic: proofs and models. CoRR (2023)
Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré
A modular construction of type theories. Log. Methods Comput. Sci. 19 (1) (2023)
Gilles Dowek
Simple Type Theory as a Clausal Theory. CoRR (2023)
Gilles Dowek
From proof theory to theories theory. CoRR (2023)
Gilles Dowek
Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View. CoRR (2023)
Gilles Dowek, Ying Jiang
Complementation: a bridge between finite and infinite proofs. CoRR (2023)
Gilles Dowek, Murdoch James Gabbay
Permissive-Nominal Logic (journal version). CoRR (2023)
Gilles Dowek
Specifying programs with propositions and with congruences. CoRR (2023)
Gilles Dowek
Preliminary investigations on induction over real numbers. CoRR (2023)
Gilles Dowek
The Undecidability of Unification Modulo σ Alone. CoRR (2023)
Gilles Dowek
The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable. CoRR (2023)
Gilles Dowek
The physical Church thesis and the sensitivity to initial conditions. CoRR (2023)
Gilles Dowek, Ying Jiang
Eigenvariables, bracketing and the decidability of positive minimal predicate logic. CoRR (2023)
Gilles Dowek
Execution traces and reduction sequences. CoRR (2023)
Gilles Dowek
A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions. CoRR (2023)
Gilles Dowek
Automatic Proof Checking and Proof Construction by Tactics. CoRR (2023)
Gilles Dowek, Alexandre Miquel
Relative normalization. CoRR (2023)
Gilles Dowek
The physical Church-Turing thesis and non deterministic computation over the real numbers. CoRR (2023)
Gilles Dowek
On the convergence of reduction-based and model-based methods in proof theory. CoRR (2023)
Gilles Dowek, Ying Jiang
On the Expressive Power of Schemes. CoRR (2023)
Gilles Dowek
Explanation: from ethics to logic. CoRR (2023)
Pablo Arrighi, Gilles Dowek
The principle of a finite density of information. CoRR (2023)
Gilles Dowek
A theory independent Curry-De Bruijn-Howard correspondence. CoRR (2023)
Gilles Dowek, Olivier Hermant
A Simple Proof That Super-Consistency Implies Cut Elimination. CoRR (2023)
Gilles Dowek
A Unification Algorithm for Second-Order Linear Terms. CoRR (2023)
Gilles Dowek, François Thiré
Logipedia: a multi-system encyclopedia of formal proofs. CoRR (2023)
Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard
Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. CoRR (2023)
Gilles Dowek
A Complete Proof Synthesis Method for the Cube of Type Systems. CoRR (2023)
Gilles Dowek, Gérard Huet, Benjamin Werner
On the Definition of the Eta-long Normal Form in Type Systems of the Cube. CoRR (2023)
Gilles Dowek, Benjamin Werner
Arithmetic as a theory modulo. CoRR (2023)
Gilles Dowek, Alexandre Miquel
Cut elimination for Zermelo set theory. CoRR (2023)
Gilles Dowek
Third Order Matching is Decidable. CoRR (2023)
Gilles Dowek
The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors. CoRR (2023)
Gilles Dowek
What do we know when we know that a theory is consistent? CoRR (2023)
Gilles Dowek, Ying Jiang
Enumerating proofs of positive formulae. CoRR (2023)
Gilles Dowek
Teaching G{ö}del's incompleteness theorems. CoRR (2023)
Denis Cousineau, Gilles Dowek
Embedding Pure Type Systems in the lambda-Pi-calculus modulo. CoRR (2023)
Guillaume Burel, Gilles Dowek
How can we prove that a proof search method is not an instance of another? CoRR (2023)
Richard Statman, Gilles Dowek
On Statman's Finite Completeness Theorem. CoRR (2023)
Gilles Dowek
Confluence as a cut elimination property. CoRR (2023)
Pablo Arrighi, Gilles Dowek, Amélia Durbec
A toy model provably featuring an arrow of time without past hypothesis. CoRR (2023)
Gilles Dowek
The Stratified Foundations as a theory modulo. CoRR (2023)
Gilles Dowek, Murdoch James Gabbay
PNL to HOL: from the logic of nominal sets to the logic of higher-order functions. CoRR (2023)
Alejandro Díaz-Caro, Gilles Dowek
Linear lambda-calculus is linear. CoRR (2022)
Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, Jiaxiang Liu
Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs. Math. Struct. Comput. Sci. 32 (7) (2022)
Gilles Dowek
From the Universality of Mathematical Truth to the Interoperability of Proof Systems. IJCAR (2022)
Alejandro Díaz-Caro, Gilles Dowek
Linear Lambda-Calculus is Linear. FSCD (2022)
Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré
Some Axioms for Mathematics. FSCD (2021)
Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré
Some axioms for mathematics. CoRR (2021)
Gilles Dowek
Interacting Safely with an Unsafe Environment. LFMTP (2021)
Alejandro Díaz-Caro, Gilles Dowek
A New Connective in Natural Deduction, and Its Application to Quantum Computing. ICTAC (2021)
Alejandro Díaz-Caro, Gilles Dowek
A New Connective in Natural Deduction, and its Application to Quantum Computing. CoRR (2020)
Alejandro Díaz-Caro, Gilles Dowek
Extensional proofs in a propositional logic modulo isomorphisms. CoRR (2020)
Ying Jiang, Jian Liu, Gilles Dowek, Kailiang Ji
Towards Combining Model Checking and Proof Checking. Comput. J. 62 (9) (2019)
Alejandro Díaz-Caro, Gilles Dowek
Proof Normalisation in a Logic Identifying Isomorphic Propositions. FSCD (2019)
Alejandro Díaz-Caro, Gilles Dowek, Juan Pablo Rinaldi
Two linearities for quantum computing in the lambda calculus. Biosyst. 186 (2019)
Gilles Dowek
Rules and Derivations in an Elementary Logic Course. FLAP 4 (1) (2017)
Alejandro Díaz-Caro, Gilles Dowek
Typing Quantum Superpositions and Measurement. TPNC (2017)
Pablo Arrighi, Gilles Dowek
Lineal: A linear-algebraic Lambda-calculus. Log. Methods Comput. Sci. 13 (1) (2017)
Gilles Dowek
Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory. ICALP (2017)
Gilles Dowek
Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems. PxTP (2017)
Jian Liu, Gilles Dowek, Kailiang Ji, Ying Jiang
SCTL: Towards Combining Model Checking and Proof Checking. CoRR (2016)
Gilles Dowek, Catherine Dubois, Brigitte Pientka, Florian Rabe
Universality of Proofs (Dagstuhl Seminar 16421). Dagstuhl Reports 6 (10) (2016)
Gilles Dowek, Ying Jiang
Decidability, Introduction Rules and Automata. CoRR (2016)
Nachum Dershowitz, Gilles Dowek
Universality in two dimensions. J. Log. Comput. 26 (1) (2016)
Gilles Dowek
Rules and derivations in an elementary logic course. CoRR (2016)
Alejandro Díaz-Caro, Gilles Dowek
Quantum superpositions and projective measurement in the lambda calculus. CoRR (2016)
Gilles Dowek
On the definition of the classical connectives and quantifiers. CoRR (2016)
Gilles Dowek
Models and termination of proof-reduction in the $λ$$Π$-calculus modulo theory. CoRR (2015)
Pablo Arrighi, Gilles Dowek
Discrete geodesics and cellular automata. CoRR (2015)
Gilles Dowek, Ying Jiang
Decidability, Introduction Rules and Automata. LPAR (2015)
Guillaume Burel, Gilles Dowek, Ying Jiang
A Completion Method to Decide Reachability in Rewrite Systems. FroCos (2015)
Gilles Dowek
Deduction modulo theory. CoRR (2015)
Pablo Arrighi, Gilles Dowek
Discrete Geodesics and Cellular Automata. TPNC (2015)
Pablo Arrighi, Gilles Dowek
Free fall and cellular automata. DCM (2015)
Cláudia Nalon, Bruno Lopes, Gilles Dowek, Edward Hermann Haeusler
A Calculus for Automatic Verification of Petri Nets Based on Resolution and Dynamic Logics. LSFA (2014)
Gilles Dowek, Ying Jiang
Cut-elimination and the decidability of reachability in alternating pushdown systems. CoRR (2014)
Cécilia Englander, Gilles Dowek, Edward Hermann Haeusler
Yet Another Bijection Between Sequent Calculus and Natural Deduction. LSFA (2014)
Alejandro Díaz-Caro, Gilles Dowek
The probability of non-confluent systems. DCM (2013)
Pablo Arrighi, Gilles Dowek
Causal graph dynamics. Inf. Comput. 223 (2013)
Gilles Dowek
Real Numbers, Chaos, and the Principle of a Bounded Density of Information. CSR (2013)
Pablo Arrighi, Gilles Dowek
Causal graph dynamics CoRR (2012)
Gilles Dowek, Murdoch James Gabbay
PNL to HOL: From the logic of nominal sets to the logic of higher-order functions. Theor. Comput. Sci. 451 (2012)

Gilles Dowek.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Gilles Dowek