65 citations · 93 across the 10 of their papers we have counts for
3 papers · 1 filter
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…
The Calculus of Algebraic Constructions
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalize…
Higher-Order Termination: from Kruskal to Computability
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut el…