Research papers

 

 

 

2023

. 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: Some axioms for mathematics, Formal Structures for Computation and Deduction, 2021.

2022

. G. Dowek, From the Universality of Mathematical Truth to the Interoperability of Proof Systems, invited talk, International Joint Conference on Automated Reasoning, 2022.
. 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.
. A. Díaz-Caro and G. Dowek, Linear lambda-calculus is linear, Formal Structures for Computation and Deduction, 2022, long version.

2021

. A. Díaz-Caro and G. Dowek, A New Connective in Natural Deduction, and its Application to Quantum Computing, 18th International Colloquium on Theoretical Aspects of Computing, Best paper award shared with Muhammad Hannan Khan, Osman Hasan, and Shahid Khan for their paper Accelerating SpMV Multiplication in Probabilistic Model Checkers using GPUs. And its long version.
. G. Dowek, Interacting safely with an unsafe environment, Logical Frameworks and Meta-Languages.

2020

. A. Díaz-Caro and G. Dowek, Extensional proofs in a propositional logic modulo isomorphisms.
. G. Dowek and F. Thiré, Logipedia: a multi-system encyclopedia of formal proofs, manuscript.

2019

. A. Díaz-Caro, G. Dowek, and J.P. Rinaldi, Two linearities for quantum computing in the lambda calculus, Biosystems, 2019 (short version Typing Quantum Superpositions and Measurement, Theory and Practice of Natural Computing, 2017).
. 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, Lecons de mathématiques d'aujourd'hui, volume 5, Cassini, 2019.
. 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, Towards Combining Model Checking and Proof Checking, The Computer Journal, 62, 9, 2019, pp. 1365–1402.

2018

. G. Dowek, Execution traces and reduction sequences.

2017

. G. Dowek, Analyzing individual proofs as the basis of interoperability between proof systems, invited talk, C. Dubois and B. Woltzenlogel Paleo (eds.), Proof eXchange for Theorem Proving, Electronic Proceedings in Theoretical Computer Science, 262, 2017, pp. 3-12.
. P. Arrighi and G. Dowek, Lineal: A linear-algebraic Lambda-calculus, Logical Methods in Computer Science, 13, 1, 2017. The note where the critical pairs are analyzed. A preliminary version has been published in P. Selinger (Ed.), International workshop on quantum programming languages, Turku Centre for Computer Science General Publication, 33, 2004, pp. 21-38.
. G. Dowek, Rules and derivations in an elementary logic course, IfCoLog Journal of Logics and their Applications, 4, 1, 2017.
. G. Dowek, Models and termination of proof-reduction, International Colloquium on Automata, Languages, and Programming, 2017.

2016

. A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard, Dedukti: a Logical Framework based on the lambda-Pi-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, Developments in Computational Models, Electronic Proceedings in Theoretical Computer Science, 204, 1-10, 2016.
. G. Burel, G. Dowek, and Y. Jiang, Automata, resolution, and cut elimination and its long version.

2015

. P. Arrighi and G. Dowek, Discrete geodesics and cellular automata, with the associated program, that uses the library Isn, Theory and Practice of Natural Computing, 2015.
. G. Dowek and Y. Jiang, Decidability, introduction rules, and automata, Logic for Programming, Artificial Intelligence and Reasoning, 2015.
. G. Burel, G. Dowek, and Y. Jiang, A completion method to decide reachability in rewrite systems, 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, Deduction modulo theory, in B. Woltzenlogel Paleo and‎ D. Delahaye (eds.) All about Proofs, Proofs for All, College Publications, 2015.

2014

. G. Dowek and Y. Jiang, Cut-elimination and the decidability of reachability in alternating pushdown systems.
. A. Díaz-Caro and G. Dowek, The probability of non-confluent systems, Development of Computational Models, Electronic Proceedings in Theoretical Computer Science, 144, 2014 pp. 1-15.

2013

. N. Dershowitz and G. Dowek, Universality in two dimensions, Journal of Logic and Computation, 2013, 10.1093/logcom/ext022 2012.
. lambda 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 talk 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.

2012

. P. Arrighi and G. Dowek, Causal Graph Dynamics, Information and Computation, 223, 78-93, 2013, 10.1016/j.ic.2012.10.019.
. A. Narkawicz, C. Muñoz, and G. Dowek, Provably Correct Conflict Prevention Bands Algorithms, Science of Computer Programming, 10.1016/j.scico.2011.07.002.
. G. Dowek and M.J. Gabbay, PNL to HOL: From the logic of nominal sets to the logic of higher-order functions, Theoretical Computer Science, 451, 2012, p. 38-69.
. G. Dowek and M.J. Gabbay, Nominal Semantics for Predicate Logic: Algebras, Substitution, Quantifiers, and Limits, Italian Convention of Computational Logic, 2012.
. P. Arrighi and G. Dowek, The principle of a finite density of information, in H. Zenil (ed.), Irreducibility and Computational Equivalence: Wolfram Science 10 Years After the Publication of A New Kind of Science, 2012.
. G. Dowek, A theory independent Curry-De Bruijn-Howard correspondence, invited talk, International Colloquium on Automata, Languages and Programming, 2012.
. G. Dowek, The physical Church-Turing thesis and non-deterministic computation over the real numbers, Philosophical Transactions of the Royal Society A, 370, 1971, 2012, pp. 3349-3358, 10.1098/rsta.2011.0322
. G. Dowek, The physical Church thesis as an explanation of the Galileo thesis, Natural Computing, 2012, 10.1007/s11047-011-9301-x.
. G. Dowek, Around the physical Church-Turing thesis: cellular automata, formal languages, and the principles of quantum theory. Tutorial notes. Language and Automata Theory and Applications, Lecture Notes in Computer Science 7183, pp. 21–37, 2012.
. 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, Notre Dame Journal of Formal Logic, 53,4, 2012, pp. 439-456.

2011

. C. Rocha, C. Muñoz, and G. Dowek, A formal library of set relations and its application to synchronous languages, Theoretical Computer Science 412, 2011, 4853-4866.
. G. Dowek and M.J. Gabbay, Permissive nominal logic, Principles and Practice of Declarative Programming, 2010, pp. 165-176. Transactions on Computational Logic (to appear).
. G. Dowek and Y. Jiang, On the expressive power of schemes, Information and Computation 209, 2011, 1231-1245.

2010

. G. Dowek, Polarized Resolution Modulo, IFIP Theoretical Computer Science, 2010.
. P. Arrighi and G. Dowek, On the completeness of quantum computation models, F. Ferreira, B. Löwe, E. Mayordomo, L. Mendes Gomes (Eds.) Computability in Europe, Lecture Notes in Computer Science 6158 Springer-Verlag, 2010, pp. 21-30.
. G. Dowek, M.J. Gabbay, and D. Mulligan, Permissive nominal terms and their unification, Logic Journal of the Interest Group in Pure and Applied Logic, 2010.

2009

. G. Dowek, La forme physique de la thèse de Church et la sensibilité aux conditions initiales, Samuel Tronçon et Jean-Baptiste Joinet Ouvrir la logique au monde, Hermann, 2009. In English: The physical Church thesis and the sensitivity to initial conditions.
. G. Burel and G. Dowek, How can we prove that a proof search method is not an instance of another? Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. ACM International Conference Proceeding Series, 2009.
. 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.

2008

. G. Dowek, Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View, in C. Benzmüller, C. Brown, J. Siekmann and R. Statman (eds.), Festschrift in Honour of Peter B. Andrews on his 70th Birthday. College Publications, 2008.
. G. Dowek, The undecidability of unification modulo sigma alone (manuscript).
. 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.

2007

. G. Dowek and C. Muñoz, Conflict Detection and Resolution for 1, 2, ..., N Aircraft, 7th AIAA Aviation Technology, Integration and Operations Conference, 2007.
. 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, Typed lambda calculi and applications, Lecture Notes in Computer Science 4583, Springer-Verlag, 2007, pp. 102-117. Long version.
. G. Dowek, Truth values algebras and proof normalization, in Th. Altenkirch and C. McBride, Types for proofs and programs, Lecture Notes in Computer Science 4502, 2007, 110-124. Long version.

2006

. G. Dowek, C. Muñoz, and V. Carreño, Formal Analysis of the Operational Concept for the Small Aircraft Transportation System, Rigorous Engineering of Fault-Tolerant Systems, LNCS 4157, 2006, pp. 306-325.
. G. Dowek and Y. Jiang, Eigenvariables, bracketing and the decidability of positive minimal predicate logic, Theoretical Computer Science, 360, 2006, pp. 193-208.

2005

. C. Muñoz and G. Dowek, Hybrid Verification of an Air Traffic Operational Concept IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation, 2005.
. C. Muñoz, R. Siminiceanu, V. Carreño, and Gilles Dowek, KB3D Reference Manual - Version 1.a NASA/TM-2005-213769, 2005.
. G. Dowek, C. Muñoz, and V. Carreño, Provably Safe Coordinated Strategy for Distributed Conflict Resolution, AIAA Guidance Navigation, and Control Conference and Exhibit, 2005.
. G. Dowek, What do we know when we know that a theory is consistent?, in R. Nieuwenhuis (Ed.), Automated Deduction, Lecture Notes in Artificial Intelligence, 3632, Springer-Verlag, 2005, pp. 1-6.
. 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.), Term rewriting and applications, Lecture Notes in Computer Science 3467, Springer-Verlag, 2005, pp. 423-437.
. 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.

2004

. G. Dowek, C. Muñoz, and V. Carreño, Abstract Model of the SATS Concept of Operations: Initial Results and Recommendations, NASA/TM-2004-213006, 2004.
. C. Muñoz, G. Dowek, and V. Carreño, Modeling and Verification of an Air Traffic Concept of Operations. Software Engineering Notes, 29, 4, 2004, pp. 175-182.

2003

. G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, 31, 2003, pp. 33-72.
. G. Dowek and B. Werner, Proof normalization modulo, The Journal of Symbolic Logic, 68, 4, 2003, pp. 1289-1316.
. C. Muñoz, R. Butler, V. Carreño and G. Dowek, Formal verification of conflict detection algorithms, International Journal on Software Tools for Technology Transfer, 4, 3, 2003, pp. 371-380. Extended version: Technical report NASA/TM-2001-210864.
. G. Dowek, Confluence as a cut elimination property, R. Nieuwenhuis (Ed.), Rewriting Technique and Applications, Lecture Notes in Computer Science, 2706, Springer-Verlag, 2003, pp 2-13.
. G. Dowek, Preliminary investigations on induction over real numbers, manuscript, 2003.

2002

. A. Geser, C. Muñoz, G. Dowek, and F. Kirchner, Air Traffic Conflict Resolution and Recovery, ICASE Report 2002-12, 2002.
. G. Dowek, What is a theory ?, invited talk at H. Alt, A. Ferreira (Eds.), Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science, 2285, pp. 50-64, 2002.
. G. Dowek, Th. Hardin, and C. Kirchner, Binding logic: proofs and models, M. Baaz and A. Voronkov (Eds.) Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Artificial Intelligence, 2514, pp. 130-144, 2002. Long version.
. È. Coste-Manière, L. Adhami, D. Bondyfalat, and G. Dowek. Formal methods for safe integration in medical robotics. Proc. of 2nd IARP/IEEE RAS joint workshop on Technical Challenge for Dependable Robots in Human Environments, 2002, pp. 236-241.
. L. Adhami, D. Bondyfalat, G. Dowek, and È. Coste-Manière. Formal verification to enforce the safety of robotically assisted surgical interventions. Surgetica CAS, 2002, ppp. 90-96.

2001

. G. Dowek, Higher-order unification and matching, A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier, 2001, pp. 1009-1062.
. G. Dowek, Th. Hardin, and C. Kirchner, HOL-lambda-sigma: an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, 11, 2001, pp. 1-25.
. G. Dowek, About folding-unfolding cuts and cuts modulo, Journal of Logic and Computation 11, 3, 2001, pp. 419-429.
. G. Dowek,The Stratified Foundations as a theory modulo, S. Abramsky (Ed.) Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 2044, Springer-Verlag, 2001.
. G. Dowek, C. Muñoz, and A. Geser, Tactical conflict detection and resolution in a 3-D airspace, Proceedings of Air Traffic Management R & D Seminar, 2001. Technical Report NASA/CR-2001-210853 and ICASE 2001-7, 2001.

2000

. G. Dowek, Th. Hardin, C. Kirchner, Higher-order unification via explicit substitutions, Information and Computation, 157, 2000, pp. 183-235.
. G. Dowek, Axioms vs. rewrite rules: from completeness to cut elimination, H. Kirchner and Ch. Ringeissen (Eds.) Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence 1794, Springer-Verlag, 2000, pp. 62-72.
. 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.) Automated Deduction in Classical and Non-Classical Logics, Lecture Notes in Artificial Intelligence 1761, Springer-Verlag, 2000, pp. 1-22.
. 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, Informatiques, enjeux, tendances et évolutions R. Jacquart (Ed.), Technique et Science Informatiques, 19, 1-2-3, 2000, pp. 195-202.

1999

. G. Dowek, Collections, sets and types, Mathematical Structures in Computer Science 9, 1999, pp. 1-15.
. G. Dowek, La part du calcul, Mémoire d'habilitation, Université de Paris 7, 1999.

1998

. G. Dowek, Proof normalization for a first-order formulation of higher-order logic, E. L. Gunter, and A. Felty (Eds.), Theorem Proving in Higher-order Logics, Lecture Notes in Computer Science 1275, Springer-Verlag, 1997, pp. 105-119. Rapport de Recherche 3383, INRIA, 1998.
. G. Dowek, Th. Hardin, C. Kirchner, and F. Pfenning, Higher-order unification via explicit substitutions: the case of higher-order patterns, M. Maher (Ed.), Joint International Conference and Symposium on Logic Programming, 1996, pp. 259-273. Rapport de Recherche 3591, INRIA, 1998.
. G. Dowek, A Type-free formalization of mathematics where proofs are objects, E. Giménez and Ch. Paulin-Mohring (Eds.), Types for Proofs and Programs, Lecture Notes in Computer Science 1512, Springer-Verlag, 1998, pp. 88-111. Rapport de Recherche 2915, INRIA, 1996.

1995

. G. Dowek, Lambda-calculus, combinators and the comprehension scheme, M. Dezani-Ciancaglini and G. Plotkin (Eds.), Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 902, Springer-Verlag, 1995, pp. 154-170. Rapport de Recherche 2565, INRIA, 1995.

1994

. G. Dowek, Third order matching is decidable, Annals of Pure and Applied Logic, 69, 1994, pp. 135-155.

1993

. G. Dowek, A complete proof synthesis method for the cube of type systems, Journal of Logic and Computation, 3, 3, 1993, pp. 287-315.
. G. Dowek, The undecidability of pattern matching in calculi where primitive recursive functions are representable, Theoretical Computer Science 107, 1993, pp. 349-356.
. G. Dowek, The undecidability of typability in the lambda-pi-calculus, M. Bezem, J.F. Groote (Eds.), Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 664, Springer-Verlag, 1993, pp. 139-145.
. G. Dowek, G. Huet, B. Werner, On the definition of the eta-long normal form in the type systems of the cube, Informal proceedings of the workshop "Types", Nijmegen, 1993.
. R.S. Boyer, G. Dowek, Towards checking proof checkers, Informal proceedings of the workshop "Types", Nijmegen, 1993.
. 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.

1992

. R. Statman, G. Dowek, On Statman's finite completeness theorem, Technical Report, CMU-CS-92-152, University of Carnegie Mellon, 1992.

1991

. G. Dowek, A second order pattern matching algorithm in the cube of typed lambda-calculi, A. Tarlecki (Ed.), Mathematical foundation of computer science, Lecture Notes in Computer Science 520, Springer-Verlag, 1991, pp. 151-160. Rapport de Recherche 1585, INRIA, 1992.
. G. Dowek, Démonstration automatique dans le calcul des constructions, Thèse de doctorat, Université de Paris 7, 1991.
. 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), Comptes rendus à l'Académie des Sciences, I, 312, 12, 1991, pp. 951-956. Erratum, ibid. I, 318, 1994, p. 873.
. G. Dowek, Automatic proof checking and proof construction by tactics, Notes for the workshop on metavariables, Cambrigde, 1991.

1990

. G. Dowek, A proof synthesis algorithm for a mathematical vernacular in a restriction of the calculus of constructions, Informal proceedings of the workshop ``Logical Frameworks'', Sophia-antipolis, 1990.
. G. Dowek, Naming and scoping in a mathematical vernacular, Rapport de Recherche 1283, INRIA, 1990.

1989

. G. Dowek, Un vernaculaire modulaire pour le calcul des constructions, Mémoire de D.E.A. / Magistère, Paris 7, 1989.
back to home page