Остановите войну!
for scientists:
default search action
Gilles Dowek
- > Home > Persons > Gilles Dowek
Publications
- 2024
- [c57]Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter:
From Rewrite Rules to Axioms in the $\lambda \varPi $-Calculus Modulo Theory. FoSSaCS (2) 2024: 3-23 - [i73]Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter:
From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory. CoRR abs/2402.09024 (2024) - 2023
- [j34]Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré:
A modular construction of type theories. Log. Methods Comput. Sci. 19(1) (2023) - [j33]Alejandro Díaz-Caro, Gilles Dowek:
A new connective in natural deduction, and its application to quantum computing. Theor. Comput. Sci. 957: 113840 (2023) - [j32]Alejandro Díaz-Caro, Gilles Dowek:
Extensional proofs in a propositional logic modulo isomorphisms. Theor. Comput. Sci. 977: 114172 (2023) - [i69]Gilles Dowek, Ying Jiang:
Complementation: a bridge between finite and infinite proofs. CoRR abs/2304.05085 (2023) - [i68]Pablo Arrighi, Gilles Dowek:
The principle of a finite density of information. CoRR abs/2304.08064 (2023) - [i66]Gilles Dowek, Olivier Hermant:
A Simple Proof That Super-Consistency Implies Cut Elimination. CoRR abs/2304.10975 (2023) - [i65]Guillaume Burel, Gilles Dowek:
How can we prove that a proof search method is not an instance of another? CoRR abs/2304.11882 (2023) - [i64]Gilles Dowek, Ying Jiang:
On the Expressive Power of Schemes. CoRR abs/2304.11892 (2023) - [i60]Gilles Dowek, François Thiré:
Logipedia: a multi-system encyclopedia of formal proofs. CoRR abs/2305.00064 (2023) - [i57]Gilles Dowek, Ying Jiang:
Enumerating proofs of positive formulae. CoRR abs/2305.01440 (2023) - [i53]Gilles Dowek, Ying Jiang:
Eigenvariables, bracketing and the decidability of positive minimal predicate logic. CoRR abs/2305.08416 (2023) - [i51]Gilles Dowek, Benjamin Werner:
A constructive proof of Skolem theorem for constructive logic. CoRR abs/2305.10016 (2023) - [i47]Gilles Dowek, Thérèse Hardin, Claude Kirchner:
Binding Logic: proofs and models. CoRR abs/2305.15782 (2023) - [i39]Pablo Arrighi, Gilles Dowek, Amélia Durbec:
A toy model provably featuring an arrow of time without past hypothesis. CoRR abs/2306.07121 (2023) - [i37]Gilles Dowek, Gérard Huet, Benjamin Werner:
On the Definition of the Eta-long Normal Form in Type Systems of the Cube. CoRR abs/2307.00854 (2023) - [i35]Richard Statman, Gilles Dowek:
On Statman's Finite Completeness Theorem. CoRR abs/2309.03602 (2023) - [i31]Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky, Octavio Malherbe:
A linear proof language for second-order intuitionistic linear logic. CoRR abs/2310.08517 (2023) - [i30]Gilles Dowek, Benjamin Werner:
Arithmetic as a theory modulo. CoRR abs/2310.10326 (2023) - [i29]Denis Cousineau, Gilles Dowek:
Embedding Pure Type Systems in the lambda-Pi-calculus modulo. CoRR abs/2310.12540 (2023) - [i28]Gilles Dowek, Alexandre Miquel:
Relative normalization. CoRR abs/2310.20248 (2023) - [i27]Gilles Dowek, Alexandre Miquel:
Cut elimination for Zermelo set theory. CoRR abs/2310.20253 (2023) - [i26]Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard:
Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. CoRR abs/2311.07185 (2023) - 2022
- [j31]Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, Jiaxiang Liu:
Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs. Math. Struct. Comput. Sci. 32(7): 898-933 (2022) - [c55]Alejandro Díaz-Caro, Gilles Dowek:
Linear Lambda-Calculus is Linear. FSCD 2022: 21:1-21:17 - [i21]Alejandro Díaz-Caro, Gilles Dowek:
Linear lambda-calculus is linear. CoRR abs/2201.11221 (2022) - 2021
- [c54]Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré:
Some Axioms for Mathematics. FSCD 2021: 20:1-20:19 - [c53]Alejandro Díaz-Caro, Gilles Dowek:
A New Connective in Natural Deduction, and Its Application to Quantum Computing. ICTAC 2021: 175-193 - [i20]Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré:
Some axioms for mathematics. CoRR abs/2111.00543 (2021) - 2020
- [i19]Alejandro Díaz-Caro, Gilles Dowek:
Extensional proofs in a propositional logic modulo isomorphisms. CoRR abs/2002.03762 (2020) - [i18]Alejandro Díaz-Caro, Gilles Dowek:
A New Connective in Natural Deduction, and its Application to Quantum Computing. CoRR abs/2012.08994 (2020) - 2019
- [j30]Alejandro Díaz-Caro, Gilles Dowek, Juan Pablo Rinaldi:
Two linearities for quantum computing in the lambda calculus. Biosyst. 186 (2019) - [j29]Ying Jiang, Jian Liu, Gilles Dowek, Kailiang Ji:
Towards Combining Model Checking and Proof Checking. Comput. J. 62(9): 1365-1402 (2019) - [c51]Alejandro Díaz-Caro, Gilles Dowek:
Proof Normalisation in a Logic Identifying Isomorphic Propositions. FSCD 2019: 14:1-14:23 - 2017
- [j27]Pablo Arrighi, Gilles Dowek:
Lineal: A linear-algebraic Lambda-calculus. Log. Methods Comput. Sci. 13(1) (2017) - [c49]Alejandro Díaz-Caro, Gilles Dowek:
Typing Quantum Superpositions and Measurement. TPNC 2017: 281-293 - 2016
- [j26]Nachum Dershowitz, Gilles Dowek:
Universality in two dimensions. J. Log. Comput. 26(1): 143-167 (2016) - [i16]Gilles Dowek, Ying Jiang:
Decidability, Introduction Rules and Automata. CoRR abs/1601.01484 (2016) - [i14]Alejandro Díaz-Caro, Gilles Dowek:
Quantum superpositions and projective measurement in the lambda calculus. CoRR abs/1601.04294 (2016) - [i13]Jian Liu, Gilles Dowek, Kailiang Ji, Ying Jiang:
SCTL: Towards Combining Model Checking and Proof Checking. CoRR abs/1606.08668 (2016) - [i12]Gilles Dowek, Catherine Dubois, Brigitte Pientka, Florian Rabe:
Universality of Proofs (Dagstuhl Seminar 16421). Dagstuhl Reports 6(10): 75-98 (2016) - 2015
- [c47]Guillaume Burel, Gilles Dowek, Ying Jiang:
A Completion Method to Decide Reachability in Rewrite Systems. FroCos 2015: 205-219 - [c46]Gilles Dowek, Ying Jiang:
Decidability, Introduction Rules and Automata. LPAR 2015: 97-111 - [c45]Pablo Arrighi, Gilles Dowek:
Discrete Geodesics and Cellular Automata. TPNC 2015: 137-149 - [c44]Pablo Arrighi, Gilles Dowek:
Free fall and cellular automata. DCM 2015: 1-10 - [i9]Pablo Arrighi, Gilles Dowek:
Discrete geodesics and cellular automata. CoRR abs/1507.06836 (2015) - 2014
- [i8]Gilles Dowek, Ying Jiang:
Cut-elimination and the decidability of reachability in alternating pushdown systems. CoRR abs/1410.8470 (2014) - 2013
- [j25]Pablo Arrighi, Gilles Dowek:
Causal graph dynamics. Inf. Comput. 223: 78-93 (2013) - [c40]Alejandro Díaz-Caro, Gilles Dowek:
The probability of non-confluent systems. DCM 2013: 1-15 - 2012
- [j24]Pablo Arrighi, Gilles Dowek:
The Physical Church-Turing Thesis and the Principles of Quantum Theory. Int. J. Found. Comput. Sci. 23(5): 1131-1146 (2012) - [j23]Olivier Bournez, Gilles Dowek:
Preface. Nat. Comput. 11(1): 1 (2012) - [j21]Gilles Dowek, Olivier Hermant:
A Simple Proof that Super-Consistency Implies Cut Elimination. Notre Dame J. Formal Log. 53(4): 439-456 (2012) - [c37]Pablo Arrighi, Gilles Dowek:
Causal Graph Dynamics. ICALP (2) 2012: 54-66 - [c35]Alejandro Díaz-Caro, Gilles Dowek:
Non determinism through type isomorphism. LSFA 2012: 137-144 - [i7]Pablo Arrighi, Gilles Dowek:
Causal graph dynamics. CoRR abs/1202.1098 (2012) - [i6]Gilles Dowek, Samson Abramsky:
What Makes Alan Turing a Great Scientist? - Introduction to the Special Theme. ERCIM News 2012(91) (2012) - 2011
- [b5]Gilles Dowek, Jean-Jacques Lévy:
Introduction to the Theory of Programming Languages. Undergraduate Topics in Computer Science, Springer 2011, ISBN 978-0-85729-075-5, pp. I-XI, 1-96 - [j17]Gilles Dowek, Ying Jiang:
On the expressive power of schemes. Inf. Comput. 209(9): 1231-1245 (2011) - [i5]Pablo Arrighi, Gilles Dowek:
The physical Church-Turing thesis and the principles of quantum theory. CoRR abs/1102.1612 (2011) - 2010
- [c34]Pablo Arrighi, Gilles Dowek:
On the Completeness of Quantum Computation Models. CiE 2010: 21-30 - [i3]Pablo Arrighi, Gilles Dowek:
On the completeness of quantum computation models. CoRR abs/1004.1027 (2010) - 2009
- [j13]Gilles Dowek, Ying Jiang:
Enumerating Proofs of Positive Formulae. Comput. J. 52(7): 799-807 (2009) - [c30]Guillaume Burel, Gilles Dowek:
How can we prove that a proof search method is not an instance of another? LFMTP 2009: 84-87 - [i2]Pablo Arrighi, Gilles Dowek:
A computational definition of the notion of vectorial space. CoRR abs/0911.4051 (2009) - 2008
- [c28]Pablo Arrighi, Gilles Dowek:
Linear-algebraic lambda-calculus: higher-order, encodings, and confluence.. RTA 2008: 17-31 - 2007
- [c27]Gilles Dowek, Olivier Hermant:
A Simple Proof That Super-Consistency Implies Cut Elimination. RTA 2007: 93-106 - [c26]Denis Cousineau, Gilles Dowek:
Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. TLCA 2007: 102-117 - 2006
- [j11]Gilles Dowek, Ying Jiang:
Eigenvariables, bracketing and the decidability of positive minimal predicate logic. Theor. Comput. Sci. 360(1-3): 193-208 (2006) - [i1]Pablo Arrighi, Gilles Dowek:
Lineal: A linear-algebraic Lambda-calculus. CoRR abs/quant-ph/0612199 (2006) - 2005
- [c21]Gilles Dowek, Benjamin Werner:
Arithmetic as a Theory Modulo. RTA 2005: 423-437 - 2004
- [c19]Pablo Arrighi, Gilles Dowek:
A Computational Definition of the Notion of Vectorial Space. WRLA 2004: 249-261 - 2003
- [j10]Gilles Dowek, Thérèse Hardin, Claude Kirchner:
Theorem Proving Modulo. J. Autom. Reason. 31(1): 33-72 (2003) - [j9]Gilles Dowek, Benjamin Werner:
Proof normalization modulo. J. Symb. Log. 68(4): 1289-1316 (2003) - [c17]Gilles Dowek, Ying Jiang:
Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic. Mathematics, Logic and Computation @ ICALP 2003: 17-29 - 2002
- [c16]Gilles Dowek, Thérèse Hardin, Claude Kirchner:
Binding Logic: Proofs and Models. LPAR 2002: 130-144 - 2001
- [j6]Gilles Dowek, Thérèse Hardin, Claude Kirchner:
HOL-λσ: an intentional first-order expression of higher-order logic. Math. Struct. Comput. Sci. 11(1): 21-45 (2001) - 2000
- [j5]Gilles Dowek, Thérèse Hardin, Claude Kirchner:
Higher Order Unification via Explicit Substitutions. Inf. Comput. 157(1-2): 183-235 (2000) - 1999
- [c11]Gilles Dowek, Thérèse Hardin, Claude Kirchner:
HOL-lambdasigma: An Intentional First-Order Expression of Higher-Order Logic. RTA 1999: 317-331 - [e2]Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, Laurent Théry:
Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings. Lecture Notes in Computer Science 1690, Springer 1999, ISBN 3-540-66463-7 [contents] - 1998
- [c9]Gilles Dowek, Benjamin Werner:
Proof Normalization Modulo. TYPES 1998: 62-77 - 1996
- [c7]Gilles Dowek, Thérèse Hardin, Claude Kirchner, Frank Pfenning:
Unification via Explicit Substitutions: The Case of Higher-Order Patterns. JICSLP 1996: 259-273 - 1995
- [c5]Gilles Dowek, Thérèse Hardin, Claude Kirchner:
Higher-Order Unification via Explicit Substitutions (Extended Abstract). LICS 1995: 366-374
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-04-15 23:24 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint