P. Arrighi, G. Dowek, A. Durbec, A toy model provably featuring an arrow of time without past hypothesis.

A. Díaz-Caro and G. Dowek, Linear lambda-calculus is linear, Formal Structures for Computation and Deduction, 2022.

A. Díaz-Caro and G. Dowek, A New Connective in Natural Deduction, and its Application to Quantum Computing, Theoretical Computer Science, 2023, pp. 113840, https://doi.org/10.1016/j.tcs.2023.113840. A short version of this paper has been published in International Colloquium on Theoretical Aspects of Computing, 2021, where it received a shared best paper award.

F. Blanqui, G. Dowek, É. Grienenberger, G. Hondet, and F. Thiré, A modular construction of type theories, Logical Methods in Computer Science, 19, 1, 2023, 12:1-12:28. Short version:

G. Dowek, G, Férey, J.-P. Jouannaud, and J. Liu Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs.

G. Dowek and A. Díaz-Caro, Proof Normalisation in a Logic Identifying Isomorphic Propositions, Formal Structures for Computation and Deduction, 2019.

G. Dowek, Algorithmes et modèles : l'histoire d'une convergence, sous la direction de Pierre Mounoud,

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

Y. Jiang, J. Liu, G. Dowek, and K. Ji, SCTL: Towards Combining Model Checking and Proof Checking, The Computer Journal, 62, 9, 2019, pp. 1365–1402.

P. Arrighi and G. Dowek, Lineal: A linear-algebraic Lambda-calculus,

G. Dowek, Rules and derivations in an elementary logic course,

G. Dowek, Models and termination of proof-reduction in the λΠ-calculus modulo theory,

G. Dowek and Y. Jiang, Complementation: a bridge between finite and infinite proofs

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

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

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

G. Dowek and Y. Jiang, Decidability, introduction rules, and automata,

G. Burel, G. Dowek, and Y. Jiang, A completion method to decide reachability in rewrite systems,

G. Dowek, On the definition of the classical connectives and quantifiers, E.H. Haeusler, W. de Campos Sanz, and B. Lopes (eds.)

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, Deduction modulo theory, in B. Woltzenlogel Paleo and D. Delahaye (eds.)

A. Díaz-Caro and G. Dowek, The probability of non-confluent systems,

H. Barendregt, W. Dekkers, R. Statman, and 11 contributors,

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 talk at

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

A. Díaz-Caro and G. Dowek, Non determinism through type isomorphism,

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,

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.

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

G. Dowek and M.J. Gabbay From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions, 2011.

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. Dowek, C. Muñoz, and C. Rocha, Rewriting Logic Semantics of a Plan Execution Language , 2010.

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, The undecidability of unification modulo sigma alone, manuscript, 2008.

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 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 G. 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.

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

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

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, 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, and 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,