G. Dowek, Analyzing individual proofs as the basis of interoperability between proof systems, invited talk at Fifth Workshop on Proof eXchange for Theorem Proving, 2017.

P. Arrighi and G. Dowek, Lineal: A linear-algebraic Lambda-calculus, Logical Methods in Computer Science, Volume 13, Issue 1, 2017. The note where the critical pairs are analyzed.

G. Dowek, Rules and derivations in an elementary logic course, The IfCoLog Journal of Logics and their Applications, 4, 1, 2017.

G. Dowek, Algorithmes et modèles : l'histoire d'une convergence, sous la direction de Pierre Mounoud, Lecons de mathématiques d'aujourd'hui, volume 5, Cassini, 2017.

A. Assaf, G. Dowek, J.-P. Jouannaud, and J. Liu, Untyped Confluence in Dependent Type Theories.

G. Dowek, Models and termination of proof-reduction,

Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard, Dedukti: a Logical Framework based on the lambda-Pi-Calculus Modulo Theory.

P. Arrighi and G. Dowek, What is the Planck constant the magnitude of?

P. Arrighi and G. Dowek, Free fall and cellular automata.

G. Burel, G. Dowek, and Y. Jiang, Automata, resolution, and cut elimination and its long version.

G. Dowek and Y. Jiang, Decidability, introduction rules, and automata, International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, 2015.

G. Burel, G. Dowek, and Y. Jiang, A completion method to decide reachability in rewrite systems, International Symposium on Frontiers of Combining Systems, 2015.

G. Dowek, On the definition of the classical connectives and quantifiers, E.H. Haeusler, W. de Campos Sanz, and B. Lopes (eds.) Why is this a Proof?, Festschrift for Luiz Carlos Pereira, College Publications, 2015.

C. Englander, G. Dowek, E.H. Haeusler, Yet Another Bijection Between Sequent Calculus and Natural Deduction, Electronic Notes in Theoretical Computer Science 312 (2015), pp. 107-124

B. Lopes, C. Nalon, and G. Dowek, A Calculus for Automatic Verification of Petri Nets Based on Resolution and Dynamic Logics, Electronic Notes in Theoretical Computer Science 312 (2015), pp. 125-141.

G. Dowek and Y. Jiang, Cut-elimination and the decidability of reachability in alternating pushdown systems.

A. Díaz-Caro and G. Dowek, Simply Typed Lambda-Calculus Modulo Type Isomorphisms.

N. Dershowitz and G. Dowek, Universality in two dimensions, Journal of Logic and Computation, 2013. doi: 10.1093/logcom/ext022 2012.

H. Barendregt, W. Dekkers, R. Statman, and 11 contributors, Lambda Calculus with Types.

G. Dowek and Y. Jiang, A logical approach to CTL.

G. Dowek, Real numbers, chaos, and the principle of a bounded density of information , invited paper at International Computer Science Symposium in Russia, 2013.

G. Dowek and Y. Jiang, Axiomatizing truth in a finite model.

A. Díaz-Caro and G. Dowek, Non determinism through type isomorphism, Logical and Semantic Frameworks, with Applications, 2013.

A. Narkawicz, C. Muñoz, and G. Dowek, Provably Correct Conflict Prevention Bands Algorithms,

G. Dowek and M.J. Gabbay, PNL to HOL: From the logic of nominal sets to the logic of higher-order functions,

G. Dowek and M.J. Gabbay, Nominal Semantics for Predicate Logic: Algebras, Substitution, Quantifiers, and Limits,

P. Arrighi and G. Dowek, The principle of a finite density of information, in H. Zenil (ed.),

G. Dowek, A theory independent Curry-De Bruijn-Howard correspondence, invited talk at the International Colloquium on Automata, Languages and Programming 2012.

G. Dowek, The physical Churchâ€“Turing thesis and non-deterministic computation over the real numbers,

G. Dowek, The physical Church thesis as an explanation of the Galileo thesis,

G. Dowek, Around the physical Church-Turing thesis: cellular automata, formal languages, and the principles of quantum theory. Tutorial notes.

P. Arrighi and G. Dowek, The physical Church-Turing thesis and the principles of quantum theory. International Journal of Foundations of Computer Science, 23, 5, 2012, 10.1142/S0129054112500153.

G. Dowek and O. Hermant, A simple proof that super-consistency implies cut elimination,

G. Dowek and M.J. Gabbay, Permissive nominal logic,

G. Dowek and Y. Jiang, On the expressive power of schemes, Information and Computation 209, 2011, 1231-1245.

P. Arrighi and G. Dowek, On the completeness of quantum computation models, F. Ferreira, B. Löwe, E. Mayordomo, L. Mendes Gomes (Eds.)

G. Dowek, M.J. Gabbay, and D. Mulligan, Permissive nominal terms and their unification,

G. Burel and G. Dowek, How can we prove that a proof search method is not an instance of another?

G. Dowek, Specifying programs with propositions and with congruences (manuscript).

G. Dowek, Simple Type Theory as a Clausal Theory (manuscript).

J. Maddalon, R. Butler, C. Muñoz, and G. Dowek, A Mathematical Analysis of Conflict Prevention Information, 9th AIAA Aviation Technology, Integration, and Operations Conference, September 2009. Extended version: A Mathematical Basis for the Safety Analysis of Conflict Prevention Algorithms, Technical Memorandum, NASA TM-2009-215768, June 2009.

J. Maddalon, R. Butler, C. Muñoz, and G. Dowek, A Mathematical Basis for the Safety Analysis of Conflict Prevention Algorithms, Technical Memorandum, NASA TM-2009-215768, June 2009.

G. Dowek, On the convergence of reduction-based and model-based methods in proof theory, Logic Journal of the Interest Group in Pure and Applied Logic, 2009.

G. Dowek and Y. Jiang, Enumerating proofs of positive formulae, The Computer Journal, 52(7), 2009, pp. 799-807.

G. Dowek, C. Muñoz, and C. Păsăreanu, A Small-Step Semantics of PLEXIL, Technical Report, 2008-11, National Institute of Aerospace, 2008.

G. Dowek, The undecidability of unification modulo sigma alone (manuscript).

G. Dowek and A. Miquel, Relative normalization (manuscript).

G. Dowek and A. Miquel, Cut elimination for Zermelo set theory (manuscript). With the proofs of 53 easy lemmas.

G. Dowek, C. Muñoz, and Corina S. Păsăreanu, A Formal Analysis Framework for PLEXIL, Third Workshop on Planning and Plan Execution for Real-World Systems, 2007.

P. Brauner, G. Dowek, and B. Wack, Normalization in Supernatural deduction and in Deduction modulo (manuscript).

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the lambda-Pi-calculus modulo, in S. Ronchi Della Rocca,

G. Dowek, Truth values algebras and proof normalization, in Th. Altenkirch and C. McBride,

G. Dowek and Y. Jiang, Eigenvariables, bracketing and the decidability of positive minimal predicate logic,

C. Muñoz, R. Siminiceanu, V. Carreño, and Gilles Dowek,

G. Dowek, C. Muñoz, and V. Carreño,

G. Dowek, What do we know when we know that a theory is consistent?, in R. Nieuwenhuis (Ed.),

G. Dowek and B. Werner, A constructive proof of Skolem theorem for constructive logic (manuscript).

G. Dowek and B. Werner, Arithmetic as a theory modulo, in J. Giesel (Ed.),

P. Arrighi and G. Dowek, A computational definition of the notion of vectorial space, N. Martí-Oliet (ed.), Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications (WRLA 2004), Electronic Notes in Theoretical Computer Science, 117, 2005, pp. 249-261.

C. Muñoz, G. Dowek, and V. Carreño, Modeling and Verification of an Air Traffic Concept of Operations.

P. Arrighi and G. Dowek, Linear-algebraic lambda-calculus. A preliminary version has been published in P. Selinger (Ed.),

G. Dowek and B. Werner, Proof normalization modulo,

C. Muñoz, R. Butler, V. Carreño and G. Dowek, Formal verification of conflict detection algorithms,

G. Dowek, Confluence as a cut elimination property, R. Nieuwenhuis (Ed.),

G. Dowek, Preliminary investigations on induction over real numbers, manuscript, 2003.

G. Dowek, What is a theory ?, invited talk at H. Alt, A. Ferreira (Eds.),

G. Dowek, Th. Hardin, and C. Kirchner, Binding logic: proofs and models, M. Baaz and A. Voronkov (Eds.)

È. Coste-Manière, L. Adhami, D. Bondyfalat, and G. Dowek. Formal methods for safe integration in medical robotics.

L. Adhami, D. Bondyfalat, G. Dowek, and È. Coste-Manière. Formal verification to enforce the safety of robotically assisted surgical interventions.

G. Dowek, Th. Hardin, and C. Kirchner, HOL-lambda-sigma: an intentional first-order expression of higher-order logic,

G. Dowek, About folding-unfolding cuts and cuts modulo,

G. Dowek,The Stratified Foundations as a theory modulo, S. Abramsky (Ed.)

G. Dowek, C. Muñoz, and A. Geser, Tactical conflict detection and resolution in a 3-D airspace, Proceedings of

G. Dowek, Axioms vs. rewrite rules: from completeness to cut elimination, H. Kirchner and Ch. Ringeissen (Eds.)

G. Dowek, Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory, R. Cafferra and G. Salzer (Eds.)

G. Dowek and B. Werner, An inconsistent theory modulo defined by a confluent and terminating rewrite system, manuscript, 2000.

G. Dowek, La vérification automatique de démonstrations,

G. Dowek, La part du calcul, Mémoire d'habilitation, Université de Paris 7, 1999.

G. Dowek, Th. Hardin, C. Kirchner, and F. Pfenning, Higher-order unification via explicit substitutions: the case of higher-order patterns, M. Maher (Ed.),

G. Dowek, A Type-free formalization of mathematics where proofs are objects, E. Giménez and Ch. Paulin-Mohring (Eds.),

G. Dowek, The undecidability of pattern matching in calculi where primitive recursive functions are representable,

G. Dowek, The undecidability of typability in the lambda-pi-calculus, M. Bezem, J.F. Groote (Eds.),

G. Dowek, G. Huet, B. Werner, On the definition of the eta-long normal form in the type systems of the cube,

R.S. Boyer, G. Dowek, Towards checking proof checkers,

G. Dowek, A unification algorithm for second-order linear terms, manuscript, 1993.

G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, Ch. Paulin-Mohring, B. Werner, The Coq proof assistant user's guide: version 5.8 INRIA Tech. report 154, 1993.

G. Dowek, Démonstration automatique dans le calcul des constructions,

G. Dowek, L'indécidabilité du filtrage du troisième ordre dans les calculs avec types dépendants ou constructeurs de types (The undecidability of third order pattern matching in calculi with dependent types or type constructors),

G. Dowek, Automatic proof checking and proof construction by tactics,

G. Dowek, Naming and scoping in a mathematical vernacular,