 | 2012 |
|---|
| 53 |       | Xiaomu Shi,
Jean-François Monin,
Frédéric Tuong,
Frédéric Blanqui:
First steps towards the certification of an ARM simulator using Compcert
CoRR abs/1202.6472: (2012) |
| 52 | | Frédéric Blanqui,
Adam Koprowski:
CoLoR: a Coq library on
CoRR abs/1202.6473: (2012) |
| 2011 |
|---|
| 51 | | Xiaomu Shi,
Jean-François Monin,
Frédéric Tuong,
Frédéric Blanqui:
First Steps towards the Certification of an ARM Simulator Using Compcert.
CPP 2011: 346-361 |
| 50 | | Frédéric Blanqui,
Claude Helmstetter,
Vania Joloboff,
Jean-François Monin,
Xiaomu Shi:
Designing a CPU model: from a pseudo-formal document to fast code
CoRR abs/1109.4351: (2011) |
| 49 | | Frédéric Blanqui,
Claude Kirchner,
Colin Riba:
On the confluence of lambda-calculus with conditional rewriting
CoRR abs/1109.4353: (2011) |
| 48 | | Sho Suzuki,
Keiichirou Kusakari,
Frédéric Blanqui:
Argument filterings and usable rules in higher-order rewrite systems
CoRR abs/1109.4357: (2011) |
| 47 | | Keiichirou Kusakari,
Yasuo Isogai,
Masahiko Sakai,
Frédéric Blanqui:
Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems
CoRR abs/1109.5468: (2011) |
| 46 | | Frédéric Blanqui,
Adam Koprowski:
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates.
Mathematical Structures in Computer Science 21(4): 827-859 (2011) |
| 2010 |
|---|
| 45 | | Frédéric Blanqui,
Claude Kirchner,
Colin Riba:
On the confluence of lambda-calculus with conditional rewriting.
Theor. Comput. Sci. 411(37): 3301-3327 (2010) |
| 2009 |
|---|
| 44 | | Frédéric Blanqui,
Cody Roux:
On the Relation between Sized-Types Based Termination and Semantic Labelling.
CSL 2009: 147-162 |
| 43 | | Frédéric Blanqui,
Cody Roux:
On the relation between size-based termination and semantic labelling
CoRR abs/0906.4173: (2009) |
| 42 | | Keiichirou Kusakari,
Yasuo Isogai,
Masahiko Sakai,
Frédéric Blanqui:
Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems.
IEICE Transactions 92-D(10): 2007-2015 (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 |
Data released under the ODC-BY 1.0 license — See also our legal information page