Gilles Dowek - RankMe

185 papers A* 3A 5B 6C 6Misc 1Journal 112Unranked 40

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Reconstruction of SMT proofs with Lambdapi. Acta Informatica Alessio Coltellacci, Bruno Andreotti, Haniel Barbosa, Gilles Dowek, Stephan Merz
2025	J	`jnl`	A new introduction rule for disjunction. CoRR Alejandro Díaz-Caro, Gilles Dowek
2024	C	`conf`	A Linear Proof Language for Second-Order Intuitionistic Linear Logic. WoLLIC Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky, Octavio Malherbe
2024	J	`jnl`	A Linear Sup-Calculus for Quantum Measurement. Bull. Comput. Data Sci. Gilles Dowek
2024	C	`conf`	A Toy Model Provably Featuring an Arrow of Time Without Past Hypothesis. RC Pablo Arrighi, Gilles Dowek, Amélia Durbec
2024	J	`jnl`	A linear linear lambda-calculus. Math. Struct. Comput. Sci. Alejandro Díaz-Caro, Gilles Dowek
2024	—	`conf`	From Rewrite Rules to Axioms in the $\lambda \varPi $-Calculus Modulo Theory. FoSSaCS (2) Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter
2024	J	`jnl`	From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory. CoRR Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter
2024	—	`conf`	Reconstruction of SMT Proofs with Lambdapi. SMT@CAV Alessio Coltellacci, Stephan Merz, Gilles Dowek
2024	J	`jnl`	Space-time deterministic graph rewriting. CoRR Pablo Arrighi, Marin Costes, Gilles Dowek, Luidnel Maignan
2023	J	`jnl`	A Complete Proof Synthesis Method for the Cube of Type Systems. CoRR Gilles Dowek
2023	J	`jnl`	A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions. CoRR Gilles Dowek
2023	J	`jnl`	A Simple Proof That Super-Consistency Implies Cut Elimination. CoRR Gilles Dowek, Olivier Hermant
2023	J	`jnl`	A Unification Algorithm for Second-Order Linear Terms. CoRR Gilles Dowek
2023	J	`jnl`	A constructive proof of Skolem theorem for constructive logic. CoRR Gilles Dowek, Benjamin Werner
2023	J	`jnl`	A linear proof language for second-order intuitionistic linear logic. CoRR Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky, Octavio Malherbe
2023	J	`jnl`	A modular construction of type theories. Log. Methods Comput. Sci. Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré
2023	J	`jnl`	A new connective in natural deduction, and its application to quantum computing. Theor. Comput. Sci. Alejandro Díaz-Caro, Gilles Dowek
2023	J	`jnl`	A theory independent Curry-De Bruijn-Howard correspondence. CoRR Gilles Dowek
2023	J	`jnl`	A toy model provably featuring an arrow of time without past hypothesis. CoRR Pablo Arrighi, Gilles Dowek, Amélia Durbec
2023	J	`jnl`	Arithmetic as a theory modulo. CoRR Gilles Dowek, Benjamin Werner
2023	J	`jnl`	Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory. CoRR Gilles Dowek
2023	J	`jnl`	Automatic Proof Checking and Proof Construction by Tactics. CoRR Gilles Dowek
2023	J	`jnl`	Axioms vs. rewrite rules: from completeness to cut elimination. CoRR Gilles Dowek
2023	J	`jnl`	Binding Logic: proofs and models. CoRR Gilles Dowek, Thérèse Hardin, Claude Kirchner
2023	J	`jnl`	Complementation: a bridge between finite and infinite proofs. CoRR Gilles Dowek, Ying Jiang
2023	J	`jnl`	Confluence as a cut elimination property. CoRR Gilles Dowek
2023	J	`jnl`	Cut elimination for Zermelo set theory. CoRR Gilles Dowek, Alexandre Miquel
2023	J	`jnl`	Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. CoRR Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard
2023	J	`jnl`	Eigenvariables, bracketing and the decidability of positive minimal predicate logic. CoRR Gilles Dowek, Ying Jiang
2023	J	`jnl`	Embedding Pure Type Systems in the lambda-Pi-calculus modulo. CoRR Denis Cousineau, Gilles Dowek
2023	J	`jnl`	Enumerating proofs of positive formulae. CoRR Gilles Dowek, Ying Jiang
2023	J	`jnl`	Execution traces and reduction sequences. CoRR Gilles Dowek
2023	J	`jnl`	Explanation: from ethics to logic. CoRR Gilles Dowek
2023	J	`jnl`	Extensional proofs in a propositional logic modulo isomorphisms. Theor. Comput. Sci. Alejandro Díaz-Caro, Gilles Dowek
2023	J	`jnl`	From proof theory to theories theory. CoRR Gilles Dowek
2023	J	`jnl`	How can we prove that a proof search method is not an instance of another? CoRR Guillaume Burel, Gilles Dowek
2023	J	`jnl`	Logipedia: a multi-system encyclopedia of formal proofs. CoRR Gilles Dowek, François Thiré
2023	J	`jnl`	Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits. CoRR Gilles Dowek, Murdoch James Gabbay
2023	J	`jnl`	On Statman's Finite Completeness Theorem. CoRR Richard Statman, Gilles Dowek
2023	J	`jnl`	On the Definition of the Eta-long Normal Form in Type Systems of the Cube. CoRR Gilles Dowek, Gérard Huet, Benjamin Werner
2023	J	`jnl`	On the Expressive Power of Schemes. CoRR Gilles Dowek, Ying Jiang
2023	J	`jnl`	On the convergence of reduction-based and model-based methods in proof theory. CoRR Gilles Dowek
2023	J	`jnl`	PNL to HOL: from the logic of nominal sets to the logic of higher-order functions. CoRR Gilles Dowek, Murdoch James Gabbay
2023	J	`jnl`	Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques. CoRR Gilles Dowek, Murdoch James Gabbay, Dominic P. Mulligan
2023	J	`jnl`	Permissive-Nominal Logic (journal version). CoRR Gilles Dowek, Murdoch James Gabbay
2023	J	`jnl`	Preliminary investigations on induction over real numbers. CoRR Gilles Dowek
2023	J	`jnl`	Relative normalization. CoRR Gilles Dowek, Alexandre Miquel
2023	J	`jnl`	Simple Type Theory as a Clausal Theory. CoRR Gilles Dowek
2023	J	`jnl`	Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View. CoRR Gilles Dowek
2023	J	`jnl`	Specifying programs with propositions and with congruences. CoRR Gilles Dowek
2023	J	`jnl`	Teaching G{ö}del's incompleteness theorems. CoRR Gilles Dowek
2023	J	`jnl`	The Stratified Foundations as a theory modulo. CoRR Gilles Dowek
2023	J	`jnl`	The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable. CoRR Gilles Dowek
2023	J	`jnl`	The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors. CoRR Gilles Dowek
2023	J	`jnl`	The Undecidability of Typability in the Lambda-Pi-Calculus. CoRR Gilles Dowek
2023	J	`jnl`	The Undecidability of Unification Modulo σ Alone. CoRR Gilles Dowek
2023	J	`jnl`	The physical Church thesis and the sensitivity to initial conditions. CoRR Gilles Dowek
2023	J	`jnl`	The physical Church-Turing thesis and non deterministic computation over the real numbers. CoRR Gilles Dowek
2023	J	`jnl`	The principle of a finite density of information. CoRR Pablo Arrighi, Gilles Dowek
2023	J	`jnl`	Third Order Matching is Decidable. CoRR Gilles Dowek
2023	J	`jnl`	Truth values algebras and proof normalization. CoRR Gilles Dowek
2023	J	`jnl`	What do we know when we know that a theory is consistent? CoRR Gilles Dowek
2023	J	`jnl`	What is a Theory ? CoRR Gilles Dowek
2022	J	`jnl`	Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs. Math. Struct. Comput. Sci. Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, Jiaxiang Liu
2022	A	`conf`	From the Universality of Mathematical Truth to the Interoperability of Proof Systems. IJCAR Gilles Dowek
2022	B	`conf`	Linear Lambda-Calculus is Linear. FSCD Alejandro Díaz-Caro, Gilles Dowek
2022	J	`jnl`	Linear lambda-calculus is linear. CoRR Alejandro Díaz-Caro, Gilles Dowek
2021	C	`conf`	A New Connective in Natural Deduction, and Its Application to Quantum Computing. ICTAC Alejandro Díaz-Caro, Gilles Dowek
2021	—	`conf`	Interacting Safely with an Unsafe Environment. LFMTP Gilles Dowek
2021	B	`conf`	Some Axioms for Mathematics. FSCD Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré
2021	J	`jnl`	Some axioms for mathematics. CoRR Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré
2020	J	`jnl`	A New Connective in Natural Deduction, and its Application to Quantum Computing. CoRR Alejandro Díaz-Caro, Gilles Dowek
2020	J	`jnl`	Extensional proofs in a propositional logic modulo isomorphisms. CoRR Alejandro Díaz-Caro, Gilles Dowek
2020	—	`ch.`	Theoretical Computer Science: Computability, Decidability and Logic. A Guided Tour of Artificial Intelligence Research (3) (III) Olivier Bournez, Gilles Dowek, Rémi Gilleron, Serge Grigorieff, Jean-Yves Marion, Simon Perdrix, Sophie Tison
2020	—	`ch.`	Theoretical Computer Science: Computational Complexity. A Guided Tour of Artificial Intelligence Research (3) (III) Olivier Bournez, Gilles Dowek, Rémi Gilleron, Serge Grigorieff, Jean-Yves Marion, Simon Perdrix, Sophie Tison
2019	B	`conf`	Proof Normalisation in a Logic Identifying Isomorphic Propositions. FSCD Alejandro Díaz-Caro, Gilles Dowek
2019	J	`jnl`	Towards Combining Model Checking and Proof Checking. Comput. J. Ying Jiang, Jian Liu, Gilles Dowek, Kailiang Ji
2019	J	`jnl`	Two linearities for quantum computing in the lambda calculus. Biosyst. Alejandro Díaz-Caro, Gilles Dowek, Juan Pablo Rinaldi
2017	—	`conf`	Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems. PxTP Gilles Dowek
2017	J	`jnl`	Lineal: A linear-algebraic Lambda-calculus. Log. Methods Comput. Sci. Pablo Arrighi, Gilles Dowek
2017	A*	`conf`	Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory. ICALP Gilles Dowek
2017	J	`jnl`	Rules and Derivations in an Elementary Logic Course. FLAP Gilles Dowek
2017	—	`conf`	Typing Quantum Superpositions and Measurement. TPNC Alejandro Díaz-Caro, Gilles Dowek
2016	J	`jnl`	Decidability, Introduction Rules and Automata. CoRR Gilles Dowek, Ying Jiang
2016	J	`jnl`	On the definition of the classical connectives and quantifiers. CoRR Gilles Dowek
2016	—	`ed.`	Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2016, Porto, Portugal, June 23, 2016 LFMTP Gilles Dowek, Daniel R. Licata, Sandra Alves
2016	J	`jnl`	Quantum superpositions and projective measurement in the lambda calculus. CoRR Alejandro Díaz-Caro, Gilles Dowek
2016	J	`jnl`	Rules and derivations in an elementary logic course. CoRR Gilles Dowek
2016	J	`jnl`	SCTL: Towards Combining Model Checking and Proof Checking. CoRR Jian Liu, Gilles Dowek, Kailiang Ji, Ying Jiang
2016	J	`jnl`	Universality in two dimensions. J. Log. Comput. Nachum Dershowitz, Gilles Dowek
2016	J	`jnl`	Universality of Proofs (Dagstuhl Seminar 16421). Dagstuhl Reports Gilles Dowek, Catherine Dubois, Brigitte Pientka, Florian Rabe
2015	—	`conf`	A Completion Method to Decide Reachability in Rewrite Systems. FroCos Guillaume Burel, Gilles Dowek, Ying Jiang
2015	B	`conf`	Decidability, Introduction Rules and Automata. LPAR Gilles Dowek, Ying Jiang
2015	J	`jnl`	Deduction modulo theory. CoRR Gilles Dowek
2015	—	`conf`	Discrete Geodesics and Cellular Automata. TPNC Pablo Arrighi, Gilles Dowek
2015	J	`jnl`	Discrete geodesics and cellular automata. CoRR Pablo Arrighi, Gilles Dowek
2015	—	`conf`	Free fall and cellular automata. DCM Pablo Arrighi, Gilles Dowek
2015	J	`jnl`	Models and termination of proof-reduction in the $λ$$Π$-calculus modulo theory. CoRR Gilles Dowek
2014	—	`conf`	A Calculus for Automatic Verification of Petri Nets Based on Resolution and Dynamic Logics. LSFA Cláudia Nalon, Bruno Lopes, Gilles Dowek, Edward Hermann Haeusler
2014	J	`jnl`	Cut-elimination and the decidability of reachability in alternating pushdown systems. CoRR Gilles Dowek, Ying Jiang
2014	—	`ed.`	Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings RTA-TLCA Gilles Dowek
2014	—	`conf`	Yet Another Bijection Between Sequent Calculus and Natural Deduction. LSFA Cécilia Englander, Gilles Dowek, Edward Hermann Haeusler
2013	J	`jnl`	Causal graph dynamics. Inf. Comput. Pablo Arrighi, Gilles Dowek
2013	Misc	`conf`	Real Numbers, Chaos, and the Principle of a Bounded Density of Information. CSR Gilles Dowek
2013	—	`conf`	The probability of non-confluent systems. DCM Alejandro Díaz-Caro, Gilles Dowek
2012	J	`jnl`	A Simple Proof that Super-Consistency Implies Cut Elimination. Notre Dame J. Formal Log. Gilles Dowek, Olivier Hermant
2012	—	`conf`	A Theory Independent Curry-De Bruijn-Howard Correspondence. ICALP (2) Gilles Dowek
2012	C	`conf`	Around the Physical Church-Turing Thesis: Cellular Automata, Formal Languages, and the Principles of Quantum Theory. LATA Gilles Dowek
2012	—	`conf`	Causal Graph Dynamics. ICALP (2) Pablo Arrighi, Gilles Dowek
2012	J	`jnl`	Causal graph dynamics CoRR Pablo Arrighi, Gilles Dowek
2012	—	`conf`	Nominal Semantics for Predicate Logic: Algebras, Substitution, Quantifiers, and Limits. CILC Gilles Dowek, Murdoch James Gabbay
2012	—	`conf`	Non determinism through type isomorphism LSFA Alejandro Díaz-Caro, Gilles Dowek
2012	J	`jnl`	PNL to HOL: From the logic of nominal sets to the logic of higher-order functions. Theor. Comput. Sci. Gilles Dowek, Murdoch James Gabbay
2012	J	`jnl`	Permissive-nominal logic: First-order logic over nominal terms and sets. ACM Trans. Comput. Log. Gilles Dowek, Murdoch James Gabbay
2012	J	`jnl`	Preface. Nat. Comput. Olivier Bournez, Gilles Dowek
2012	J	`jnl`	Provably correct conflict prevention bands algorithms. Sci. Comput. Program. Anthony Narkawicz, César A. Muñoz, Gilles Dowek
2012	J	`jnl`	The Physical Church-Turing Thesis and the Principles of Quantum Theory. Int. J. Found. Comput. Sci. Pablo Arrighi, Gilles Dowek
2012	J	`jnl`	The physical Church thesis as an explanation of the Galileo thesis. Nat. Comput. Gilles Dowek
2012	J	`jnl`	What Makes Alan Turing a Great Scientist? - Introduction to the Special Theme. ERCIM News Gilles Dowek, Samson Abramsky
2011	J	`jnl`	A formal library of set relations and its application to synchronous languages. Theor. Comput. Sci. Camilo Rocha, César A. Muñoz, Gilles Dowek
2011	J	`jnl`	From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions. CoRR Gilles Dowek, Murdoch Gabbay
2011	—	`book`	Introduction to the Theory of Programming Languages. Gilles Dowek, Jean-Jacques Lévy
2011	J	`jnl`	On the expressive power of schemes. Inf. Comput. Gilles Dowek, Ying Jiang
2011	—	`book`	Proofs and Algorithms - An Introduction to Logic and Computability. Gilles Dowek
2011	J	`jnl`	The physical Church-Turing thesis and the principles of quantum theory CoRR Pablo Arrighi, Gilles Dowek
2010	—	`conf`	How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project. NASA Formal Methods Ricky W. Butler, George Hagen, Jeffrey Maddalon, César A. Muñoz, Anthony Narkawicz, Gilles Dowek
2010	C	`conf`	On the Completeness of Quantum Computation Models. CiE Pablo Arrighi, Gilles Dowek
2010	J	`jnl`	On the completeness of quantum computation models CoRR Pablo Arrighi, Gilles Dowek
2010	J	`jnl`	Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques. Log. J. IGPL Gilles Dowek, Murdoch James Gabbay, Dominic P. Mulligan
2010	C	`conf`	Permissive-nominal logic. PPDP Gilles Dowek, Murdoch James Gabbay
2010	—	`conf`	Polarized Resolution Modulo. IFIP TCS Gilles Dowek
2010	J	`jnl`	Preface. J. Autom. Reason. Alessandro Armando, Peter Baumgartner, Gilles Dowek
2009	J	`jnl`	A computational definition of the notion of vectorial space CoRR Pablo Arrighi, Gilles Dowek
2009	J	`jnl`	Enumerating Proofs of Positive Formulae. Comput. J. Gilles Dowek, Ying Jiang
2009	—	`conf`	How can we prove that a proof search method is not an instance of another? LFMTP Guillaume Burel, Gilles Dowek
2009	J	`jnl`	On the convergence of reduction-based and model-based methods in proof theory. Log. J. IGPL Gilles Dowek
2009	—	`book`	Principles of Programming Languages. Gilles Dowek
2009	—	`conf`	Rewriting Logic Semantics of a Plan Execution Language SOS Gilles Dowek, César A. Muñoz, Camilo Rocha
2008	A	`ed.`	Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings IJCAR Alessandro Armando, Peter Baumgartner, Gilles Dowek
2008	—	`conf`	Linear-algebraic lambda-calculus: higher-order, encodings, and confluence.. RTA Pablo Arrighi, Gilles Dowek
2007	—	`conf`	A Simple Proof That Super-Consistency Implies Cut Elimination. RTA Gilles Dowek, Olivier Hermant
2007	—	`conf`	Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. TLCA Denis Cousineau, Gilles Dowek
2007	—	`conf`	On the Convergence of Reduction-based and Model-based Methods in Proof Theory. LSFA Gilles Dowek
2006	J	`jnl`	Eigenvariables, bracketing and the decidability of positive minimal predicate logic. Theor. Comput. Sci. Gilles Dowek, Ying Jiang
2006	—	`conf`	Formal Analysis of the Operational Concept for the Small Aircraft Transportation System. RODIN Book César A. Muñoz, Victor Carreño, Gilles Dowek
2006	J	`jnl`	Lineal: A linear-algebraic Lambda-calculus. CoRR Pablo Arrighi, Gilles Dowek
2006	—	`conf`	Truth Values Algebras and Proof Normalization. TYPES Gilles Dowek
2005	—	`conf`	Arithmetic as a Theory Modulo. RTA Gilles Dowek, Benjamin Werner
2005	A	`conf`	What Do We Know When We Know That a Theory Is Consistent?. CADE Gilles Dowek
2004	—	`conf`	A Computational Definition of the Notion of Vectorial Space. WRLA Pablo Arrighi, Gilles Dowek
2004	A	`conf`	Modeling and verification of an air traffic concept of operations. ISSTA César A. Muñoz, Gilles Dowek, Victor Carreño
2003	—	`conf`	Confluence as a Cut Elimination Property. RTA Gilles Dowek
2003	—	`conf`	Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic. Mathematics, Logic and Computation @ ICALP Gilles Dowek, Ying Jiang
2003	J	`jnl`	Formal verification of conflict detection algorithms. Int. J. Softw. Tools Technol. Transf. César A. Muñoz, Victor Carreño, Gilles Dowek, Ricky W. Butler
2003	J	`jnl`	Proof normalization modulo. J. Symb. Log. Gilles Dowek, Benjamin Werner
2003	J	`jnl`	Theorem Proving Modulo. J. Autom. Reason. Gilles Dowek, Thérèse Hardin, Claude Kirchner
2002	B	`conf`	Binding Logic: Proofs and Models. LPAR Gilles Dowek, Thérèse Hardin, Claude Kirchner
2002	A	`conf`	What Is a Theory? STACS Gilles Dowek
2001	J	`jnl`	About Folding-Unfolding Cuts and Cuts Modulo. J. Log. Comput. Gilles Dowek
2001	—	`conf`	Formal Verification of Conflict Detection Algorithms. CHARME Ricky W. Butler, Victor Carreño, Gilles Dowek, César A. Muñoz
2001	J	`jnl`	HOL-λσ: an intentional first-order expression of higher-order logic. Math. Struct. Comput. Sci. Gilles Dowek, Thérèse Hardin, Claude Kirchner
2001	—	`ch.`	Higher-Order Unification and Matching. Handbook of Automated Reasoning Gilles Dowek
2001	—	`conf`	The Stratified Foundations as a Theory Modulo. TLCA Gilles Dowek
2000	—	`conf`	Axioms vs. Rewrite Rules: From Completeness to Cut Elimination. FroCoS Gilles Dowek
2000	J	`jnl`	Higher Order Unification via Explicit Substitutions. Inf. Comput. Gilles Dowek, Thérèse Hardin, Claude Kirchner
1999	J	`jnl`	Collections, sets and types. Math. Struct. Comput. Sci. Gilles Dowek
1999	—	`conf`	HOL- RTA Gilles Dowek, Thérèse Hardin, Claude Kirchner
1999	—	`book`	La part du calcul. Gilles Dowek
1999	—	`ed.`	Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings TPHOLs Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, Laurent Théry
1998	—	`conf`	Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory. FTP (LNCS Selection) Gilles Dowek
1998	—	`conf`	Proof Normalization Modulo. TYPES Gilles Dowek, Benjamin Werner
1997	—	`conf`	Proof Normalization for a First-Order Formulation of Higher-Order Logic. TPHOLs Gilles Dowek
1996	—	`conf`	A Type-Free Formalization of Mathematics where Proofs are Objects. TYPES Gilles Dowek
1996	—	`ed.`	Higher-Order Algebra, Logic, and Term Rewriting, Second International Workshop, HOA '95, Paderborn, Germany, September 21-22, 1995, Selected Papers HOA Gilles Dowek, Jan Heering, Karl Meinke, Bernhard Möller
1996	—	`conf`	Unification via Explicit Substitutions: The Case of Higher-Order Patterns. JICSLP Gilles Dowek, Thérèse Hardin, Claude Kirchner, Frank Pfenning
1995	A*	`conf`	Higher-Order Unification via Explicit Substitutions (Extended Abstract) LICS Gilles Dowek, Thérèse Hardin, Claude Kirchner
1995	—	`conf`	Lambda-calculus, Combinators and the Comprehension Scheme. TLCA Gilles Dowek
1994	J	`jnl`	Third Order Matching is Decidable. Ann. Pure Appl. Log. Gilles Dowek
1993	J	`jnl`	A Complete Proof Synthesis Method for the Cube of Type Systems. J. Log. Comput. Gilles Dowek
1993	J	`jnl`	The Undecidability of Pattern Matching in Calculi Where Primitive Recursive Functions are Representable. Theor. Comput. Sci. Gilles Dowek
1993	—	`conf`	The Undecidability of Typability in the Lambda-Pi-Calculus. TLCA Gilles Dowek
1992	A*	`conf`	Third Order Matching is Decidable LICS Gilles Dowek
1991	B	`conf`	A Second-Order Pattern Matching Algorithm for the Cube of Typed Lambda-Calculi. MFCS Gilles Dowek
1991	—	`—`	Démonstration Automatique dans le Calcul des Constructions. (Automated Theorem Proving in the Calculus of Constructions). Gilles Dowek