default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDGilles Dowek
- > Home > Persons > Gilles Dowek
Publications
- 2023
[i72]Gilles Dowek:
Teaching G{ö}del's incompleteness theorems. CoRR abs/2303.18099 (2023)- [i71]Gilles Dowek:
Explanation: from ethics to logic. CoRR abs/2304.00821 (2023) - [i70]Gilles Dowek:
Execution traces and reduction sequences. CoRR abs/2304.05039 (2023) - [i67]Gilles Dowek:
A theory independent Curry-De Bruijn-Howard correspondence. CoRR abs/2304.08068 (2023) - [i63]Gilles Dowek:
The physical Church thesis and the sensitivity to initial conditions. CoRR abs/2304.13318 (2023) - [i62]Gilles Dowek:
Simple Type Theory as a Clausal Theory. CoRR abs/2304.13319 (2023) - [i61]Gilles Dowek:
Specifying programs with propositions and with congruences. CoRR abs/2304.13321 (2023) - [i59]Gilles Dowek:
The physical Church-Turing thesis and non deterministic computation over the real numbers. CoRR abs/2305.01432 (2023) - [i58]Gilles Dowek:
On the convergence of reduction-based and model-based methods in proof theory. CoRR abs/2305.01439 (2023) - [i56]Gilles Dowek:
Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View. CoRR abs/2305.03322 (2023) - [i55]Gilles Dowek:
The Undecidability of Unification Modulo σ Alone. CoRR abs/2305.06214 (2023) - [i54]Gilles Dowek:
Truth values algebras and proof normalization. CoRR abs/2305.07311 (2023) - [i52]Gilles Dowek:
What do we know when we know that a theory is consistent? CoRR abs/2305.10012 (2023) - [i50]Gilles Dowek:
Confluence as a cut elimination property. CoRR abs/2305.13790 (2023) - [i49]Gilles Dowek:
Preliminary investigations on induction over real numbers. CoRR abs/2305.14803 (2023) - [i48]Gilles Dowek:
What is a Theory ? CoRR abs/2305.15780 (2023) - [i46]Gilles Dowek:
The Stratified Foundations as a theory modulo. CoRR abs/2305.18837 (2023) - [i45]Gilles Dowek:
From proof theory to theories theory. CoRR abs/2306.00478 (2023) - [i44]Gilles Dowek:
Axioms vs. rewrite rules: from completeness to cut elimination. CoRR abs/2306.00495 (2023) - [i43]Gilles Dowek:
Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory. CoRR abs/2306.00498 (2023) - [i42]Gilles Dowek:
Third Order Matching is Decidable. CoRR abs/2306.01473 (2023) - [i41]Gilles Dowek:
A Complete Proof Synthesis Method for the Cube of Type Systems. CoRR abs/2306.05835 (2023) - [i40]Gilles Dowek:
The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable. CoRR abs/2306.05876 (2023) - [i38]Gilles Dowek:
The Undecidability of Typability in the Lambda-Pi-Calculus. CoRR abs/2306.07599 (2023) - [i36]Gilles Dowek:
A Unification Algorithm for Second-Order Linear Terms. CoRR abs/2309.02024 (2023) - [i34]Gilles Dowek:
The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors. CoRR abs/2309.11819 (2023) - [i33]Gilles Dowek:
Automatic Proof Checking and Proof Construction by Tactics. CoRR abs/2309.16224 (2023) - [i32]Gilles Dowek:
A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions. CoRR abs/2310.04090 (2023) - 2022
- [c56]Gilles Dowek:
From the Universality of Mathematical Truth to the Interoperability of Proof Systems. IJCAR 2022: 8-11 - 2021
- [c52]Gilles Dowek:
Interacting Safely with an Unsafe Environment. LFMTP 2021: 30-38 - 2017
- [j28]Gilles Dowek:
Rules and Derivations in an Elementary Logic Course. FLAP 4(1) (2017) - [c50]Gilles Dowek
:
Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory. ICALP 2017: 109:1-109:14 - [c48]Gilles Dowek:
Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems. PxTP 2017: 3-12 - 2016
- [i17]Gilles Dowek:
Rules and derivations in an elementary logic course. CoRR abs/1601.01483 (2016) - [i15]Gilles Dowek:
On the definition of the classical connectives and quantifiers. CoRR abs/1601.01782 (2016) - 2015
- [i11]Gilles Dowek:
Models and termination of proof-reduction in the $λ$$Π$-calculus modulo theory. CoRR abs/1501.06522 (2015) - [i10]Gilles Dowek:
Deduction modulo theory. CoRR abs/1501.06523 (2015) - 2014
- [e4]Gilles Dowek:
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. Lecture Notes in Computer Science 8560, Springer 2014, ISBN 978-3-319-08917-1 [contents] - 2013
- [c41]Gilles Dowek:
Real Numbers, Chaos, and the Principle of a Bounded Density of Information. CSR 2013: 347-353 - 2012
- [j22]Gilles Dowek:
The physical Church thesis as an explanation of the Galileo thesis. Nat. Comput. 11(2): 247-251 (2012) - [c38]Gilles Dowek:
A Theory Independent Curry-De Bruijn-Howard Correspondence. ICALP (2) 2012: 13-15 - [c36]Gilles Dowek:
Around the Physical Church-Turing Thesis: Cellular Automata, Formal Languages, and the Principles of Quantum Theory. LATA 2012: 21-37 - 2011
- [b4]Gilles Dowek:
Proofs and Algorithms - An Introduction to Logic and Computability. Undergraduate Topics in Computer Science, Springer 2011, ISBN 978-0-85729-120-2, pp. I-XII, 1-155 - 2010
- [c33]Gilles Dowek:
Polarized Resolution Modulo. IFIP TCS 2010: 182-196 - 2009
- [b3]Gilles Dowek:
Principles of Programming Languages. Undergraduate Topics in Computer Science, Springer 2009, ISBN 978-1-84882-031-9 - [j12]Gilles Dowek:
On the convergence of reduction-based and model-based methods in proof theory. Log. J. IGPL 17(5): 489-497 (2009) - 2007
- [c25]Gilles Dowek:
On the Convergence of Reduction-based and Model-based Methods in Proof Theory. LSFA 2007: 137-144 - 2006
- [c23]Gilles Dowek:
Truth Values Algebras and Proof Normalization. TYPES 2006: 110-124 - 2005
- [c22]Gilles Dowek:
What Do We Know When We Know That a Theory Is Consistent?. CADE 2005: 1-6 - 2003
- [c18]Gilles Dowek:
Confluence as a Cut Elimination Property. RTA 2003: 2-13 - 2002
- [c15]Gilles Dowek:
What Is a Theory? STACS 2002: 50-64 - 2001
- [j7]Gilles Dowek:
About Folding-Unfolding Cuts and Cuts Modulo. J. Log. Comput. 11(3): 419-429 (2001) - [c13]Gilles Dowek:
The Stratified Foundations as a Theory Modulo. TLCA 2001: 136-150 - [p1]Gilles Dowek:
Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009-1062 - 2000
- [c12]Gilles Dowek:
Axioms vs. Rewrite Rules: From Completeness to Cut Elimination. FroCoS 2000: 62-72 - 1999
- [b2]Gilles Dowek:
La part du calcul. Paris Diderot University, France, 1999 - [j4]Gilles Dowek:
Collections, sets and types. Math. Struct. Comput. Sci. 9(1): 109-123 (1999) - 1998
- [c10]Gilles Dowek:
Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory. FTP (LNCS Selection) 1998: 1-22 - 1997
- [c8]Gilles Dowek:
Proof Normalization for a First-Order Formulation of Higher-Order Logic. TPHOLs 1997: 105-119 - 1996
- [c6]Gilles Dowek:
A Type-Free Formalization of Mathematics where Proofs are Objects. TYPES 1996: 88-111 - 1995
- [c4]Gilles Dowek:
Lambda-calculus, Combinators and the Comprehension Scheme. TLCA 1995: 154-170 - 1994
- [j3]Gilles Dowek:
Third Order Matching is Decidable. Ann. Pure Appl. Log. 69(2-3): 135-155 (1994) - 1993
- [j2]Gilles Dowek:
A Complete Proof Synthesis Method for the Cube of Type Systems. J. Log. Comput. 3(3): 287-315 (1993) - [j1]Gilles Dowek:
The Undecidability of Pattern Matching in Calculi Where Primitive Recursive Functions are Representable. Theor. Comput. Sci. 107(2): 349-356 (1993) - [c3]Gilles Dowek:
The Undecidability of Typability in the Lambda-Pi-Calculus. TLCA 1993: 139-145 - 1992
- [c2]Gilles Dowek:
Third Order Matching is Decidable. LICS 1992: 2-10 - 1991
- [b1]Gilles Dowek:
Démonstration Automatique dans le Calcul des Constructions. (Automated Theorem Proving in the Calculus of Constructions). Paris Diderot University, France, 1991 - [c1]Gilles Dowek:
A Second-Order Pattern Matching Algorithm for the Cube of Typed Lambda-Calculi. MFCS 1991: 151-160
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-07 22:28 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
