- CSB - MetaPress - Google - Bing - Yahoo
 | 2012 | |
|---|---|---|
| i30 |      | 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) |
| i29 | | |
| i28 | | Frédéric Blanqui, Kim Quyen Ly: Automated verification of termination certificates. CoRR abs/1212.2350 (2012) |
| 2011 | ||
| j6 | | 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) |
| c18 | | 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 |
| i27 | | 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) |
| i26 | | Frédéric Blanqui, Claude Kirchner, Colin Riba: On the confluence of lambda-calculus with conditional rewriting. CoRR abs/1109.4353 (2011) |
| i25 | | Sho Suzuki, Keiichirou Kusakari, Frédéric Blanqui: Argument filterings and usable rules in higher-order rewrite systems. CoRR abs/1109.4357 (2011) |
| i24 | | 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) |
| 2010 | ||
| j5 | | 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 | ||
| j4 | | 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) |
| c17 | | |
| i23 | | Frédéric Blanqui, Cody Roux: On the relation between size-based termination and semantic labelling. CoRR abs/0906.4173 (2009) |
| 2008 | ||
| c16 | | Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio: The Computability Path Ordering: The End of a Quest. CSL 2008: 1-14 |
| c15 | | 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 |
| i22 | | 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) |
| i21 | | Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio: The computability path ordering: the end of a quest. CoRR abs/0806.2517 (2008) |
| 2007 | ||
| c14 | | Frédéric Blanqui: Computability Closure: Ten Years Later. Rewriting, Computation and Proof 2007: 68-88 |
| c13 | | Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub: Building Decision Procedures in the Calculus of Inductive Constructions. CSL 2007: 328-342 |
| c12 | | 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 |
| c11 | | Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio: HORPO with Computability Closure: A Reconstruction. LPAR 2007: 138-150 |
| i20 | | Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub: Building Decision Procedures in the Calculus of Inductive Constructions. CoRR abs/0707.1266 (2007) |
| i19 | | |
| i18 | | Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio: HORPO with Computability Closure : A Reconstruction. CoRR abs/0708.3582 (2007) |
| i17 | | 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 | ||
| c10 | | Frédéric Blanqui, Claude Kirchner, Colin Riba: On the Confluence of lambda-Calculus with Conditional Rewriting. FoSSaCS 2006: 382-397 |
| c9 | | Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio: Higher-Order Termination: From Kruskal to Computability. LPAR 2006: 1-14 |
| c8 | | 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 |
| i16 | | Frédéric Blanqui: Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations. CoRR abs/cs/0608125 (2006) |
| i15 | | Frédéric Blanqui, Claude Kirchner, Colin Riba: On the confluence of lambda-calculus with conditional rewriting. CoRR abs/cs/0609002 (2006) |
| i14 | | 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) |
| i13 | | |
| i12 | | Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio: Higher-Order Termination: from Kruskal to Computability. CoRR abs/cs/0609039 (2006) |
| i11 | | Frédéric Blanqui: A type-based termination criterion for dependently-typed higher-order rewrite systems. CoRR abs/cs/0610062 (2006) |
| i10 | | Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada: The Calculus of Algebraic Constructions. CoRR abs/cs/0610063 (2006) |
| i9 | | Frédéric Blanqui: Termination and Confluence of Higher-Order Rewrite Systems. CoRR abs/cs/0610064 (2006) |
| i8 | | Frédéric Blanqui: Definitions by Rewriting in the Calculus of Constructions. CoRR abs/cs/0610065 (2006) |
| i7 | | Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada: Inductive-data-type Systems. CoRR abs/cs/0610066 (2006) |
| i6 | | |
| i5 | | Frédéric Blanqui: An Isabelle formalization of protocol-independent secrecy with an application to e-commerce. CoRR abs/cs/0610069 (2006) |
| i4 | | Frédéric Blanqui: Inductive types in the Calculus of Algebraic Constructions. CoRR abs/cs/0610070 (2006) |
| i3 | | |
| i2 | | Frédéric Blanqui: Definitions by rewriting in the Calculus of Constructions. CoRR abs/cs/0610072 (2006) |
| i1 | | Frédéric Blanqui: Inductive types in the Calculus of Algebraic Constructions. CoRR abs/cs/0610073 (2006) |
| 2005 | ||
| j3 | | Frédéric Blanqui: Inductive types in the Calculus of Algebraic Constructions. Fundam. Inform. 65(1-2): 61-86 (2005) |
| j2 | | Frédéric Blanqui: Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science 15(1): 37-92 (2005) |
| c7 | | Frédéric Blanqui: Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations. CSL 2005: 135-150 |
| 2004 | ||
| c6 | | Frédéric Blanqui: A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems. RTA 2004: 24-39 |
| 2003 | ||
| c5 | | |
| c4 | | |
| 2002 | ||
| j1 | | Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada: Inductive-data-type systems. Theor. Comput. Sci. 272(1-2): 41-68 (2002) |
| 2001 | ||
| c3 | | |
| 2000 | ||
| c2 | | |
| 1999 | ||
| c1 | | Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada: The Calculus of algebraic Constructions. RTA 1999: 301-316 |
Colors in the list of coauthors
Last update Mon May 20 10:57:53 2013 CET by the DBLP Team —
Data released under the ODC-BY 1.0 license — See also our legal information page