| 2008 |
|---|
| 42 | | Alessandro Armando,
Peter Baumgartner,
Gilles Dowek:
Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings
Springer 2008 |
| 41 | EE | Pablo Arrighi,
Gilles Dowek:
Linear-algebraic lambda-calculus: higher-order, encodings, and confluence..
RTA 2008: 17-31 |
| 40 | EE | Gilles Dowek:
On the Convergence of Reduction-based and Model-based Methods in Proof Theory.
Electr. Notes Theor. Comput. Sci. 205: 137-144 (2008) |
| 2007 |
|---|
| 39 | EE | Gilles Dowek,
Olivier Hermant:
A Simple Proof That Super-Consistency Implies Cut Elimination.
RTA 2007: 93-106 |
| 38 | EE | Denis Cousineau,
Gilles Dowek:
Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo.
TLCA 2007: 102-117 |
| 2006 |
|---|
| 37 | EE | César Muñoz,
Victor Carreño,
Gilles Dowek:
Formal Analysis of the Operational Concept for the Small Aircraft Transportation System.
RODIN Book 2006: 306-325 |
| 36 | EE | Gilles Dowek:
Truth Values Algebras and Proof Normalization.
TYPES 2006: 110-124 |
| 35 | EE | Gilles Dowek,
Ying Jiang:
Eigenvariables, bracketing and the decidability of positive minimal predicate logic.
Theor. Comput. Sci. 360(1-3): 193-208 (2006) |
| 2005 |
|---|
| 34 | EE | Gilles Dowek:
What Do We Know When We Know That a Theory Is Consistent?.
CADE 2005: 1-6 |
| 33 | EE | Gilles Dowek,
Benjamin Werner:
Arithmetic as a Theory Modulo.
RTA 2005: 423-437 |
| 32 | EE | Pablo Arrighi,
Gilles Dowek:
A Computational Definition of the Notion of Vectorial Space.
Electr. Notes Theor. Comput. Sci. 117: 249-261 (2005) |
| 2004 |
|---|
| 31 | EE | César Muñoz,
Gilles Dowek,
Victor Carreño:
Modeling and verification of an air traffic concept of operations.
ISSTA 2004: 175-182 |
| 2003 |
|---|
| 30 | EE | Gilles Dowek:
Confluence as a Cut Elimination Property.
RTA 2003: 2-13 |
| 29 | EE | Gilles Dowek,
Ying Jiang:
Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic.
Electr. Notes Theor. Comput. Sci. 85(7): (2003) |
| 28 | EE | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner:
Theorem Proving Modulo.
J. Autom. Reasoning 31(1): 33-72 (2003) |
| 27 | EE | César Muñoz,
Victor Carreño,
Gilles Dowek,
Ricky W. Butler:
Formal verification of conflict detection algorithms.
STTT 4(3): 371-380 (2003) |
| 2002 |
|---|
| 26 | EE | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner:
Binding Logic: Proofs and Models.
LPAR 2002: 130-144 |
| 25 | EE | Gilles Dowek:
What Is a Theory?
STACS 2002: 50-64 |
| 2001 |
|---|
| 24 | EE | Ricky W. Butler,
Victor Carreño,
Gilles Dowek,
César Muñoz:
Formal Verification of Conflict Detection Algorithms.
CHARME 2001: 403-417 |
| 23 | EE | Gilles Dowek:
The Stratified Foundations as a Theory Modulo.
TLCA 2001: 136-150 |
| 22 | | Gilles Dowek:
Higher-Order Unification and Matching.
Handbook of Automated Reasoning 2001: 1009-1062 |
| 21 | EE | Gilles Dowek:
About Folding-Unfolding Cuts and Cuts Modulo.
J. Log. Comput. 11(3): 419-429 (2001) |
| 20 | | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner:
HOL-[lambda][sigma]: an intentional first-order expression of higher-order logic.
Mathematical Structures in Computer Science 11(1): 21-45 (2001) |
| 2000 |
|---|
| 19 | | Gilles Dowek:
Axioms vs. Rewrite Rules: From Completeness to Cut Elimination.
FroCos 2000: 62-72 |
| 18 | | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner:
Higher Order Unification via Explicit Substitutions.
Inf. Comput. 157(1-2): 183-235 (2000) |
| 1999 |
|---|
| 17 | | Yves Bertot,
Gilles Dowek,
André Hirschowitz,
C. Paulin,
Laurent Théry:
Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings
Springer 1999 |
| 16 | EE | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner:
HOL-lambdasigma: An Intentional First-Order Expression of Higher-Order Logic.
RTA 1999: 317-331 |
| 15 | | Gilles Dowek:
Collections, sets and types.
Mathematical Structures in Computer Science 9(1): 109-123 (1999) |
| 1998 |
|---|
| 14 | EE | 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 |
| 13 | EE | Gilles Dowek,
Benjamin Werner:
Proof Normalization Modulo.
TYPES 1998: 62-77 |
| 1997 |
|---|
| 12 | | Gilles Dowek:
Proof Normalization for a First-Order Formulation of Higher-Order Logic.
TPHOLs 1997: 105-119 |
| 1996 |
|---|
| 11 | | Gilles Dowek,
Jan Heering,
Karl Meinke,
Bernhard Möller:
Higher-Order Algebra, Logic, and Term Rewriting, Second International Workshop, HOA '95, Paderborn, Germany, September 21-22, 1995, Selected Papers
Springer 1996 |
| 10 | | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner,
Frank Pfenning:
Unification via Explicit Substitutions: The Case of Higher-Order Patterns.
JICSLP 1996: 259-273 |
| 9 | | Gilles Dowek:
A Type-Free Formalization of Mathematics where Proofs are Objects.
TYPES 1996: 88-111 |
| 1995 |
|---|
| 8 | | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner:
Higher-Order Unification via Explicit Substitutions (Extended Abstract)
LICS 1995: 366-374 |
| 7 | | Gilles Dowek:
Lambda-calculus, Combinators and the Comprehension Scheme.
TLCA 1995: 154-170 |
| 1994 |
|---|
| 6 | | Gilles Dowek:
Third Order Matching is Decidable.
Ann. Pure Appl. Logic 69(2-3): 135-155 (1994) |
| 1993 |
|---|
| 5 | | Gilles Dowek:
The Undecidability of Typability in the Lambda-Pi-Calculus.
TLCA 1993: 139-145 |
| 4 | | Gilles Dowek:
A Complete Proof Synthesis Method for the Cube of Type Systems.
J. Log. Comput. 3(3): 287-315 (1993) |
| 3 | | Gilles Dowek:
The Undecidability of Pattern Matching in Calculi Where Primitive Recursive Functions are Representable.
Theor. Comput. Sci. 107(2): 349-356 (1993) |
| 1992 |
|---|
| 2 | | Gilles Dowek:
Third Order Matching is Decidable
LICS 1992: 2-10 |
| 1991 |
|---|
| 1 | | Gilles Dowek:
A Second-Order Pattern Matching Algorithm for the Cube of Typed Lambda-Calculi.
MFCS 1991: 151-160 |
