×

zbMATH — the first resource for mathematics

Dowek, Gilles

Compute Distance To:
Author ID: dowek.gilles Recent zbMATH articles by "Dowek, Gilles"
Published as: Dowek, Gilles
External Links: MGP · Wikidata · IdRef · theses.fr
Documents Indexed: 89 Publications since 1991, including 19 Books
Reviewing Activity: 5 Reviews
Biographic References: 1 Publication

Publications by Year

Citations contained in zbMATH Open

49 Publications have been cited 260 times in 159 Documents Cited by Year
Theorem proving modulo. Zbl 1049.03011
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
48
2003
Higher order unification via explicit substitutions. Zbl 1005.03016
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
22
2000
Third order matching is decidable. Zbl 0822.03010
Dowek, Gilles
12
1994
HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic. Zbl 0972.03012
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
11
2001
Proof normalization modulo. Zbl 1059.03062
Dowek, Gilles; Werner, Benjamin
11
2003
Embedding pure type systems in the lambda-pi-calculus modulo. Zbl 1215.03021
Cousineau, Denis; Dowek, Gilles
11
2007
Higher-order unification and matching. Zbl 1011.03005
Dowek, Gilles
11
2001
Arithmetic as a theory modulo. Zbl 1078.03046
Dowek, Gilles; Werner, Benjamin
10
2005
Linear-algebraic \(\lambda \)-calculus: Higher-order, encodings, and confluence. Zbl 1146.68027
Arrighi, Pablo; Dowek, Gilles
10
2008
A complete proof synthesis method for the cube of type systems. Zbl 0789.68123
Dowek, Gilles
8
1993
Eigenvariables, bracketing and the decidability of positive minimal predicate logic. Zbl 1106.03006
Dowek, Gilles; Jiang, Ying
8
2006
Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques. Zbl 1215.03048
Dowek, Gilles; Gabbay, Murdoch J.; Mulligan, Dominic P.
8
2010
Confluence as a cut elimination property. Zbl 1038.03054
Dowek, Gilles
7
2003
Polarized resolution modulo. Zbl 1202.68215
Dowek, Gilles
7
2010
Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12–15, 2008 Proceedings. Zbl 1149.68003
Armando, Alessandro (ed.); Baumgartner, Peter (ed.); Dowek, Gilles (ed.)
6
2008
A second-order pattern matching algorithm for the cube of typed \(\lambda\)-calculi. Zbl 0764.68045
Dowek, Gilles
6
1991
Truth values algebras and proof normalization. Zbl 1178.03074
Dowek, Gilles
5
2007
What is a theory? Zbl 1054.03026
Dowek, Gilles
4
2002
A simple proof that super-consistency implies cut elimination. Zbl 1203.03086
Dowek, Gilles; Hermant, Olivier
4
2007
The undecidability of typability in the lambda-pi-calculus. Zbl 0788.68017
Dowek, Gilles
3
1993
Automatic proofs in the calculus of constructions. (Démonstration automatique dans le calcul des constructions.) Zbl 0849.68111
Dowek, Gilles
3
1991
The principles of programming languages. (Les principes des langages de programmation.) Zbl 1193.68066
Dowek, Gilles
3
2008
Binding logic: Proofs and models. Zbl 1023.03023
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
3
2002
A computational definition of the notion of vectorial space. Zbl 1272.68166
Arrighi, Pablo; Dowek, Gilles
3
2005
Permissive-nominal logic: first-order logic over nominal terms and sets. Zbl 1352.03042
Dowek, Gilles; Gabbay, Murdoch J.
3
2012
Lineal: a linear-algebraic \(\lambda\)-calculus. Zbl 1448.68206
Arrighi, Pablo; Dowek, Gilles
3
2017
Proof normalization for a first-order formulation of higher-order logic. Zbl 0905.03036
Dowek, Gilles
2
1997
HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic. Zbl 0944.03007
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
2
1999
Rewriting and typed lambda calculi. Joint international conference, RTA-TLCA 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Zbl 1291.68017
Dowek, Gilles (ed.)
2
2014
Causal graph dynamics. Zbl 1367.37008
Arrighi, Pablo; Dowek, Gilles
2
2012
About folding-unfolding cuts and cuts modulo. Zbl 0986.03045
Dowek, Gilles
2
2001
Principles of programming languages. Zbl 1187.68116
Dowek, Gilles
2
2009
Yet another bijection between sequent calculus and natural deduction. Zbl 1343.03042
Englander, Cecilia; Dowek, Gilles; Haeusler, Edward Hermann
2
2015
Automated theorem proving in first-order logic modulo: On the difference between type theory and set theory. Zbl 0960.03008
Dowek, Gilles
1
2000
Proof normalization modulo. Zbl 0944.03052
Dowek, Gilles; Werner, Benjamin
1
1999
Theorem proving in higher order logics. 12th international conference, TPHOLs ’99. Nice, France, September 14–17, 1999. Proceedings. Zbl 0929.00038
Bertot, Yves (ed.); Dowek, Gilles (ed.); Hirschowitz, André (ed.); Paulin, Christine (ed.); Théry, Laurent (ed.)
1
1999
Provably correct conflict prevention bands algorithms. Zbl 1243.68153
Narkawicz, Anthony; Muñoz, César; Dowek, Gilles
1
2012
PNL to HOL: from the logic of nominal sets to the logic of higher-order functions. Zbl 1309.03013
Dowek, Gilles; Gabbay, Murdoch J.
1
2012
Causal graph dynamics. Zbl 1272.68284
Arrighi, Pablo; Dowek, Gilles
1
2013
Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic. Zbl 1264.03039
Dowek, Gilles; Jiang, Ying
1
2003
Proofs and algorithms. An introduction to logic and computability. Zbl 1230.03001
Dowek, Gilles
1
2011
Computation, proof, machine. Mathematics enters a new age. Translated from the French by Pierre Guillot and Marion Roman. Zbl 1318.01002
Dowek, Gilles
1
2015
A formal library of set relations and its application to synchronous languages. Zbl 1229.68051
Rocha, Camilo; Muñoz, César; Dowek, Gilles
1
2011
L’indécidabilité du filtrage du troisième ordre dans les calculs avec types dépen- dants ou constructeurs de types. (The undecidability of third order pattern matching in calculi with dependent types or type constructors). Zbl 0761.03007
Dowek, Gilles
1
1991
The undecidability of pattern matching in calculi where primitive recursive functions are representable. Zbl 0773.03011
Dowek, Gilles
1
1993
Collections, sets and types. Zbl 0937.03010
Dowek, Gilles
1
1999
Skolemization in simple type theory: the logical and the theoretical points of view. Zbl 1226.03016
Dowek, Gilles
1
2008
The physical Church-Turing thesis and non-deterministic computation over the real numbers. Zbl 1329.03080
Dowek, Gilles
1
2012
The physical Church thesis as an explanation of the Galileo thesis. Zbl 1339.03007
Dowek, Gilles
1
2012
Lineal: a linear-algebraic \(\lambda\)-calculus. Zbl 1448.68206
Arrighi, Pablo; Dowek, Gilles
3
2017
Yet another bijection between sequent calculus and natural deduction. Zbl 1343.03042
Englander, Cecilia; Dowek, Gilles; Haeusler, Edward Hermann
2
2015
Computation, proof, machine. Mathematics enters a new age. Translated from the French by Pierre Guillot and Marion Roman. Zbl 1318.01002
Dowek, Gilles
1
2015
Rewriting and typed lambda calculi. Joint international conference, RTA-TLCA 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Zbl 1291.68017
Dowek, Gilles
2
2014
Causal graph dynamics. Zbl 1272.68284
Arrighi, Pablo; Dowek, Gilles
1
2013
Permissive-nominal logic: first-order logic over nominal terms and sets. Zbl 1352.03042
Dowek, Gilles; Gabbay, Murdoch J.
3
2012
Causal graph dynamics. Zbl 1367.37008
Arrighi, Pablo; Dowek, Gilles
2
2012
Provably correct conflict prevention bands algorithms. Zbl 1243.68153
Narkawicz, Anthony; Muñoz, César; Dowek, Gilles
1
2012
PNL to HOL: from the logic of nominal sets to the logic of higher-order functions. Zbl 1309.03013
Dowek, Gilles; Gabbay, Murdoch J.
1
2012
The physical Church-Turing thesis and non-deterministic computation over the real numbers. Zbl 1329.03080
Dowek, Gilles
1
2012
The physical Church thesis as an explanation of the Galileo thesis. Zbl 1339.03007
Dowek, Gilles
1
2012
Proofs and algorithms. An introduction to logic and computability. Zbl 1230.03001
Dowek, Gilles
1
2011
A formal library of set relations and its application to synchronous languages. Zbl 1229.68051
Rocha, Camilo; Muñoz, César; Dowek, Gilles
1
2011
Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques. Zbl 1215.03048
Dowek, Gilles; Gabbay, Murdoch J.; Mulligan, Dominic P.
8
2010
Polarized resolution modulo. Zbl 1202.68215
Dowek, Gilles
7
2010
Principles of programming languages. Zbl 1187.68116
Dowek, Gilles
2
2009
Linear-algebraic \(\lambda \)-calculus: Higher-order, encodings, and confluence. Zbl 1146.68027
Arrighi, Pablo; Dowek, Gilles
10
2008
Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12–15, 2008 Proceedings. Zbl 1149.68003
Armando, Alessandro; Baumgartner, Peter; Dowek, Gilles
6
2008
The principles of programming languages. (Les principes des langages de programmation.) Zbl 1193.68066
Dowek, Gilles
3
2008
Skolemization in simple type theory: the logical and the theoretical points of view. Zbl 1226.03016
Dowek, Gilles
1
2008
Embedding pure type systems in the lambda-pi-calculus modulo. Zbl 1215.03021
Cousineau, Denis; Dowek, Gilles
11
2007
Truth values algebras and proof normalization. Zbl 1178.03074
Dowek, Gilles
5
2007
A simple proof that super-consistency implies cut elimination. Zbl 1203.03086
Dowek, Gilles; Hermant, Olivier
4
2007
Eigenvariables, bracketing and the decidability of positive minimal predicate logic. Zbl 1106.03006
Dowek, Gilles; Jiang, Ying
8
2006
Arithmetic as a theory modulo. Zbl 1078.03046
Dowek, Gilles; Werner, Benjamin
10
2005
A computational definition of the notion of vectorial space. Zbl 1272.68166
Arrighi, Pablo; Dowek, Gilles
3
2005
Theorem proving modulo. Zbl 1049.03011
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
48
2003
Proof normalization modulo. Zbl 1059.03062
Dowek, Gilles; Werner, Benjamin
11
2003
Confluence as a cut elimination property. Zbl 1038.03054
Dowek, Gilles
7
2003
Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic. Zbl 1264.03039
Dowek, Gilles; Jiang, Ying
1
2003
What is a theory? Zbl 1054.03026
Dowek, Gilles
4
2002
Binding logic: Proofs and models. Zbl 1023.03023
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
3
2002
HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic. Zbl 0972.03012
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
11
2001
Higher-order unification and matching. Zbl 1011.03005
Dowek, Gilles
11
2001
About folding-unfolding cuts and cuts modulo. Zbl 0986.03045
Dowek, Gilles
2
2001
Higher order unification via explicit substitutions. Zbl 1005.03016
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
22
2000
Automated theorem proving in first-order logic modulo: On the difference between type theory and set theory. Zbl 0960.03008
Dowek, Gilles
1
2000
HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic. Zbl 0944.03007
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
2
1999
Proof normalization modulo. Zbl 0944.03052
Dowek, Gilles; Werner, Benjamin
1
1999
Theorem proving in higher order logics. 12th international conference, TPHOLs ’99. Nice, France, September 14–17, 1999. Proceedings. Zbl 0929.00038
Bertot, Yves; Dowek, Gilles; Hirschowitz, André; Paulin, Christine; Théry, Laurent
1
1999
Collections, sets and types. Zbl 0937.03010
Dowek, Gilles
1
1999
Proof normalization for a first-order formulation of higher-order logic. Zbl 0905.03036
Dowek, Gilles
2
1997
Third order matching is decidable. Zbl 0822.03010
Dowek, Gilles
12
1994
A complete proof synthesis method for the cube of type systems. Zbl 0789.68123
Dowek, Gilles
8
1993
The undecidability of typability in the lambda-pi-calculus. Zbl 0788.68017
Dowek, Gilles
3
1993
The undecidability of pattern matching in calculi where primitive recursive functions are representable. Zbl 0773.03011
Dowek, Gilles
1
1993
A second-order pattern matching algorithm for the cube of typed \(\lambda\)-calculi. Zbl 0764.68045
Dowek, Gilles
6
1991
Automatic proofs in the calculus of constructions. (Démonstration automatique dans le calcul des constructions.) Zbl 0849.68111
Dowek, Gilles
3
1991
L’indécidabilité du filtrage du troisième ordre dans les calculs avec types dépen- dants ou constructeurs de types. (The undecidability of third order pattern matching in calculi with dependent types or type constructors). Zbl 0761.03007
Dowek, Gilles
1
1991
all top 5

Cited by 208 Authors

12 Dowek, Gilles
8 Gabbay, Murdoch James
8 Kirchner, Claude
6 Arrighi, Pablo
6 Ayala-Rincón, Mauricio
6 Burel, Guillaume
6 Díaz-Caro, Alejandro
5 Cavalcanti de Moura, Flávio Leonardo
4 Hermant, Olivier
4 Jiang, Ying
4 Kaliszyk, Cezary
4 Kamareddine, Fairouz D.
4 Meseguer Guaita, José
4 Zorzi, Margherita
3 Delahaye, David
3 Fernández, Maribel
3 Houtmann, Clément
3 Kirchner, Hélène
3 Levy, Jordi
3 Miller, Dale Allen
3 Urban, Josef
3 Urzyczyn, Paweł
2 Baral, Chitta R.
2 Benzmüller, Christoph Ewald
2 Blanchette, Jasmin Christian
2 Blanqui, Frédéric
2 Bury, Guillaume
2 Cauderlier, Raphaël
2 Chihani, Zakaria
2 Dal Lago, Ugo
2 Dershowitz, Nachum
2 Dunfield, Joshua
2 Felty, Amy P.
2 Gabbay, Michael J.
2 Gonzalez, Marcos Alvarez
2 Gottesman, Aaron
2 Haeusler, Edward Hermann
2 Halmagrand, Pierre
2 Hetzl, Stefan
2 Kesner, Delia
2 Kutsia, Temur
2 Leitsch, Alexander
2 Liquori, Luigi
2 Malherbe, Octavio
2 Martí-Oliet, Narciso
2 Masini, Andrea
2 Muñoz, César A.
2 Nadathur, Gopalan
2 Nahon, Fabrice
2 Naibo, Alberto
2 Paolini, Luca
2 Paulson, Lawrence Charles
2 Pitts, Andrew M.
2 Platzer, André
2 Popescu, Andrei
2 Rocha-Oliveira, Ana Cristina
2 Roşu, Grigore
2 Schubert, Aleksy
2 Urban, Christian
2 Valiron, Benoît
2 Villaret, Mateu
2 Weller, Daniel S.
2 Woltzenlogel Paleo, Bruno
2 Yoshida, Nobuko
1 Abramsky, Samson
1 Acar, Umut A.
1 Aiguier, Marc
1 Alagi, Gábor
1 Barbosa, Haniel
1 Baumgartner, Alexander
1 Bentkamp, Alexander
1 Boldo, Sylvie
1 Bolognesi, Tommaso
1 Bonacina, Maria Paola
1 Borovanský, Peter
1 Boy de la Tour, Thierry
1 Brady, Edwin C.
1 Brauner, Paul
1 Brunel, Aloïs
1 Bruni, Roberto
1 Capecchi, Sara
1 Cerna, David M.
1 Chen, Yan
1 Ciancia, Vincenzo
1 Cirstea, Horatiu
1 Cooper, Stuart Barry
1 Cruanes, Simon
1 Czajka, Łukasz
1 de Barros Santos, Jefferson
1 de Moor, Oege
1 Dominguez, Jesus M.
1 Dubois, Catherine
1 Durán, Francisco
1 Durbec, Nicolas
1 Dzifcak, Juraj
1 Eker, Steven
1 Emmanuel, Aurélien
1 Escobar, Santiago
1 Färber, Michael
1 Faure, Germain
...and 108 more Authors

Citations by Year

Wikidata Timeline

The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.