Research papers
2023
V. Blot, G. Dowek, T. Traversié, and T. Winterhalter,
From Rewrite Rules to
Axioms in the λΠ-Calculus Modulo Theory.
A. Díaz-Caro, G. Dowek, M. Ivnisky, O. Malherbe,
A
linear proof language for second-order intuitionistic linear logic.
A. Díaz-Caro and G. Dowek,
Extensional
proofs in a propositional logic modulo isomorphisms,
Theoretical Computer Science, 2023, https://doi.org/10.1016/j.tcs.2023.114172.
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: 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.
2021
G. Dowek,
Interacting safely with an unsafe environment,
Logical Frameworks and Meta-Languages.
2020
G. Dowek and F. Thiré,
Logipedia: a
multi-system encyclopedia of formal proofs.
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,
SCTL: 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.
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
in the λΠ-calculus modulo theory,
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.
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.
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, 77, 10-11, 2012, pp. 1039-1057.
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, 37, 2011, pp. 4853-4866.
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,
Principles and Practice of Declarative Programming, 2010,
pp. 165-176.
Transactions on Computational Logic.
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: an infinite, co-infinite approach to nominal
techniques,
Logic Journal of the Interest Group in Pure and Applied Logic, 2010.
G. Dowek, C. Muñoz,
and C. Rocha,
Rewriting Logic Semantics of a Plan Execution Language
, 2010.
A. Narkawicz, C. Muñoz, and G. Dowek,
Formal verification of air traffic prevention bands algorithms,
Technical Memorandum, NASA/TM-2010-216706, 2010.
R. Butler, G. Hagen, J. Maddalon, C. Muñoz, A. Narkawicz,
and G. Dowek,
How
Formal Methods Impels Discovery:
A Short History of an Air Traffic Management Project,
Technical Memorandum, NASA/CP-2010-216215, 2010.
2009
G. Dowek, The physical
Church thesis and the sensitivity to initial conditions.
En français:
La forme physique de la thèse
de Church et la sensibilité
aux conditions initiales, in
Samuel Tronçon et Jean-Baptiste Joinet,
Ouvrir la logique au monde, Hermann, 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.
G. Dowek,
Simple Type Theory
as a Clausal Theory.
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,
2009. Extended version: 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, 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, 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.
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.
G. Dowek and A. Miquel,
Cut elimination
for Zermelo set theory. 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.
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.
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.
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 G. 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.
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
P. Arrighi and G. Dowek,
Linear-algebraic
lambda-calculus, P. Selinger (Ed.),
International workshop on quantum programming languages,
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.
International Symposium on Software Testing and Analysis,
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, 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.
È. 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, 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.
Extended
version: 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,
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, 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, and 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, 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 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