65 citations · 211 across the 36 of their papers we have counts for
12 papers · 2 filters
Inductive types in the Calculus of Algebraic Constructions
Frédéric Blanqui
In a previous work, we proved that an important part of the Calculus of Inductive Constructions (CIC), the basis of the Coq proof assistant, can be seen as a Calculus of Algebraic…
An Isabelle formalization of protocol-independent secrecy with an application to e-commerce
Frédéric Blanqui
A protocol-independent secrecy theorem is established and applied to several non-trivial protocols. In particular, it is applied to protocols proposed for protecting the computatio…
Termination and Confluence of Higher-Order Rewrite Systems
Frédéric Blanqui
In the last twenty years, several approaches to higher-order rewriting have been proposed, among which Klop's Combinatory Rewrite Systems (CRSs), Nipkow's Higher-order Rewrite Syst…
A type-based termination criterion for dependently-typed higher-order rewrite systems
Frederic Blanqui
Several authors devised type-based termination criteria for ML-like languages allowing non-structural recursive calls. We extend these works to general rewriting and dependent type…
Type theory and rewriting
Frédéric Blanqui
We study the properties, in particular termination, of dependent types systems for lambda calculus and rewriting.
Inductive-data-type Systems
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
In a previous work ("Abstract Data Type Systems", TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system an…