`Travelled to:`

1 × Estonia

1 × Germany

1 × Italy

1 × Japan

1 × Poland

1 × The Netherlands

2 × Austria

2 × France

2 × Spain

2 × USA

2 × United Kingdom

`Collaborated with:`

∅ P.Arrighi T.Hardin C.Kirchner M.J.Gabbay O.Hermant D.Cousineau B.Werner F.Pfenning

`Talks about:`

theori (6) order (6) calculus (4) higher (4) modulo (3) substitut (2) confluenc (2) principl (2) explicit (2) quantum (2)

## Person: Gilles Dowek

### DBLP: Dowek:Gilles

### Facilitated 2 volumes:

### Contributed to:

### Wrote 19 papers:

- ICALP-v2-2012-ArrighiD #graph
- Causal Graph Dynamics (PA, GD), pp. 54–66.
- ICALP-v2-2012-Dowek #independence
- A Theory Independent Curry-De Bruijn-Howard Correspondence (GD), pp. 13–15.
- LATA-2012-Dowek #automaton #formal method #physics #quantum
- Around the Physical Church-Turing Thesis: Cellular Automata, Formal Languages, and the Principles of Quantum Theory (GD), pp. 21–37.
- DLT-J-2011-ArrighiD12 #physics #quantum
- The Physical Church-Turing Thesis and the Principles of Quantum Theory (PA, GD), pp. 1131–1146.
- PPDP-2010-DowekG #logic
- Permissive-nominal logic (GD, MJG), pp. 165–176.
- RTA-2008-ArrighiD #algebra #confluence #encoding #higher-order #λ-calculus
- Linear-algebraic λ-calculus: higher-order, encodings, and confluence (PA, GD), pp. 17–31.
- RTA-2007-DowekH #proving
- A Simple Proof That Super-Consistency Implies Cut Elimination (GD, OH), pp. 93–106.
- TLCA-2007-CousineauD #calculus #type system
- Embedding Pure Type Systems in the λ-π-Calculus Modulo (DC, GD), pp. 102–117.
- CADE-2005-Dowek #consistency #question #what
- What Do We Know When We Know That a Theory Is Consistent? (GD), pp. 1–6.
- RTA-2005-DowekW #modulo theories
- Arithmetic as a Theory Modulo (GD, BW), pp. 423–437.
- WRLA-2004-ArrighiD05
- A Computational Definition of the Notion of Vectorial Space (PA, GD), pp. 249–261.
- RTA-2003-Dowek #confluence
- Confluence as a Cut Elimination Property (GD), pp. 2–13.
- TLCA-2001-Dowek #modulo theories
- The Stratified Foundations as a Theory Modulo (GD), pp. 136–150.
- RTA-1999-DowekHK #first-order #higher-order #logic #named
- HOL-λσ: An Intentional First-Order Expression of Higher-Order Logic (GD, TH, CK), pp. 317–331.
- JICSLP-1996-DowekHKP #higher-order #unification
- Unification via Explicit Substitutions: The Case of Higher-Order Patterns (GD, TH, CK, FP), pp. 259–273.
- LICS-1995-DowekHK #higher-order #unification
- Higher-Order Unification via Explicit Substitutions (GD, TH, CK), pp. 366–374.
- TLCA-1995-Dowek #combinator #comprehension #λ-calculus
- λ-calculus, Combinators and the Comprehension Scheme (GD), pp. 154–170.
- TLCA-1993-Dowek #calculus
- The Undecidability of Typability in the λ-π-Calculus (GD), pp. 139–145.
- LICS-1992-Dowek #decidability #higher-order
- Third Order Matching is Decidable (GD), pp. 2–10.