 | 2009 |
|---|
| 43 |       | Frédéric Blanqui,
Cody Roux:
On the Relation between Sized-Types Based Termination and Semantic Labelling.
CSL 2009: 147-162 |
| 42 | | Frédéric Blanqui,
Cody Roux:
On the relation between size-based termination and semantic labelling
CoRR abs/0906.4173: (2009) |
| 2008 |
|---|
| 41 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Albert Rubio:
The Computability Path Ordering: The End of a Quest.
CSL 2008: 1-14 |
| 40 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Pierre-Yves Strub:
From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures.
IFIP TCS 2008: 349-365 |
| 39 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Pierre-Yves Strub:
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
CoRR abs/0804.3762: (2008) |
| 38 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Albert Rubio:
The computability path ordering: the end of a quest
CoRR abs/0806.2517: (2008) |
| 2007 |
|---|
| 37 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Pierre-Yves Strub:
Building Decision Procedures in the Calculus of Inductive Constructions.
CSL 2007: 328-342 |
| 36 | | Frédéric Blanqui,
Thérèse Hardin,
Pierre Weis:
On the Implementation of Construction Functions for Non-free Concrete Data Types.
ESOP 2007: 95-109 |
| 35 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Albert Rubio:
HORPO with Computability Closure: A Reconstruction.
LPAR 2007: 138-150 |
| 34 | | Frédéric Blanqui:
Computability Closure: Ten Years Later.
Rewriting, Computation and Proof 2007: 68-88 |
| 33 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Pierre-Yves Strub:
Building Decision Procedures in the Calculus of Inductive Constructions
CoRR abs/0707.1266: (2007) |
| 32 | | Frédéric Blanqui:
Computability Closure: Ten Years Later
CoRR abs/0707.1372: (2007) |
| 31 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Albert Rubio:
HORPO with Computability Closure : A Reconstruction
CoRR abs/0708.3582: (2007) |
| 30 | | Frédéric Blanqui,
Thérèse Hardin,
Pierre Weis:
On the implementation of construction functions for non-free concrete data types
CoRR abs/cs/0701031: (2007) |
| 2006 |
|---|
| 29 | | Frédéric Blanqui,
Claude Kirchner,
Colin Riba:
On the Confluence of lambda-Calculus with Conditional Rewriting.
FoSSaCS 2006: 382-397 |
| 28 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Albert Rubio:
Higher-Order Termination: From Kruskal to Computability.
LPAR 2006: 1-14 |
| 27 | | Frédéric Blanqui,
Colin Riba:
Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems.
LPAR 2006: 105-119 |
| 26 | | Frédéric Blanqui:
Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations
CoRR abs/cs/0608125: (2006) |
| 25 | | Frédéric Blanqui,
Claude Kirchner,
Colin Riba:
On the confluence of lambda-calculus with conditional rewriting
CoRR abs/cs/0609002: (2006) |
| 24 | | Frédéric Blanqui,
Colin Riba:
Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems
CoRR abs/cs/0609013: (2006) |
| 23 | | Frédéric Blanqui:
(HO)RPO Revisited
CoRR abs/cs/0609037: (2006) |
| 22 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Albert Rubio:
Higher-Order Termination: from Kruskal to Computability
CoRR abs/cs/0609039: (2006) |
| 21 | | Frédéric Blanqui:
A type-based termination criterion for dependently-typed higher-order rewrite systems
CoRR abs/cs/0610062: (2006) |
| 20 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Mitsuhiro Okada:
The Calculus of Algebraic Constructions
CoRR abs/cs/0610063: (2006) |
| 19 | | Frédéric Blanqui:
Termination and Confluence of Higher-Order Rewrite Systems
CoRR abs/cs/0610064: (2006) |
| 18 | | Frédéric Blanqui:
Definitions by Rewriting in the Calculus of Constructions
CoRR abs/cs/0610065: (2006) |
| 17 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Mitsuhiro Okada:
Inductive-data-type Systems
CoRR abs/cs/0610066: (2006) |
| 16 | | Frédéric Blanqui:
Type theory and rewriting
CoRR abs/cs/0610068: (2006) |
| 15 | | Frédéric Blanqui:
An Isabelle formalization of protocol-independent secrecy with an application to e-commerce
CoRR abs/cs/0610069: (2006) |
| 14 | | Frédéric Blanqui:
Inductive types in the Calculus of Algebraic Constructions
CoRR abs/cs/0610070: (2006) |
| 13 | | Frédéric Blanqui:
Rewriting modulo in Deduction modulo
CoRR abs/cs/0610071: (2006) |
| 12 | | Frédéric Blanqui:
Definitions by rewriting in the Calculus of Constructions
CoRR abs/cs/0610072: (2006) |
| 11 | | Frédéric Blanqui:
Inductive types in the Calculus of Algebraic Constructions
CoRR abs/cs/0610073: (2006) |
| 2005 |
|---|
| 10 | | Frédéric Blanqui:
Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations.
CSL 2005: 135-150 |
| 9 | | Frédéric Blanqui:
Inductive types in the Calculus of Algebraic Constructions.
Fundam. Inform. 65(1-2): 61-86 (2005) |
| 8 | | Frédéric Blanqui:
Definitions by rewriting in the Calculus of Constructions.
Mathematical Structures in Computer Science 15(1): 37-92 (2005) |
| 2004 |
|---|
| 7 | | Frédéric Blanqui:
A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems.
RTA 2004: 24-39 |
| 2003 |
|---|
| 6 | | Frédéric Blanqui:
Rewriting Modulo in Deduction Modulo.
RTA 2003: 395-409 |
| 5 | | Frédéric Blanqui:
Inductive Types in the Calculus of Algebraic Constructions.
TLCA 2003: 46-59 |
| 2002 |
|---|
| 4 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Mitsuhiro Okada:
Inductive-data-type systems.
Theor. Comput. Sci. 272(1-2): 41-68 (2002) |
| 2001 |
|---|
| 3 |  | Frédéric Blanqui:
Definitions by Rewriting in the Calculus of Constructions.
LICS 2001: 9-18 |
| 2000 |
|---|
| 2 | | Frédéric Blanqui:
Termination and Confluence of Higher-Order Rewrite Systems.
RTA 2000: 47-61 |
| 1999 |
|---|
| 1 | | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Mitsuhiro Okada:
The Calculus of algebraic Constructions.
RTA 1999: 301-316 |
