Research papers

 

 

 

2010

. G. Dowek, Polarized Resolution Modulo (manuscript).
. P. Arrighi and G. Dowek, On the completeness of quantum computation models (manuscript).
. G. Dowek and Y. Jiang, On the expressive power of schemes (manuscript).

2009

. 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, C. Muñoz, and C. Rocha, Rewriting Logic Semantics of a Plan Execution Language, Technical Memorandum, NASA TM-2009-215770, June 2009. Structural Operational Semantics 2009.
. G. Dowek, M.J. Gabbay, and D. Mulligan, Permissive nominal terms and their unification CILC, 24th Italian Conference on Computational Logic, 2009.
. 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. Studies in Logic and the Foundations of Mathematics.
. 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, C. Muñoz, and C. Păsăreanu, A Small-Step Semantics of PLEXIL, Technical Report, 2008-11, National Institute of Aerospace, 2008.
. P. Arrighi and G. Dowek, Linear-algebraic lambda-calculus: higher-order, encodings and confluence in A. Voronkov, Rewriting techniques and applications, Lecture Notes in Computer Science, Springer-Verlag, 2008. long version.
. G. Dowek, The undecidability of unification modulo sigma alone (manuscript).

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).
. G. Dowek and O. Hermant, A simple proof that super-consistency implies cut elimination, in F. Baader, Rewriting techniques and applications, Lecture Notes in Computer Science, 4533, Springer-Verlag, 2007, pp. 93-106.
. 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.
. P. Arrighi and G. Dowek, Linear-algebraic lambda-calculus. 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.

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. (More on the Handbook here and there.)
. 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