The Calculus of Algebraic Constructions

Simple item page
dc.creatorBlanqui, Frédéric
dc.creatorJouannaud, Jean-Pierre
dc.creatorOkada, Mitsuhiro
dc.date2006-10-11
dc.date2008-05-27
dc.date.accessioned2026-07-07T09:40:57Z
dc.date.available2026-07-07T09:40:57Z
dc.descriptionThis 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 generalizes inductive types equipped with higher-order primitive recursion, by providing definitions of functions by pattern-matching which capture recursor definitions for arbitrary non-dependent and non-polymorphic inductive types satisfying a strictly positivity condition. CAC also generalizes the first-order framework of abstract data types by providing dependent types and higher-order rewrite rules.
dc.identifierhttps://arxiv.org/abs/cs/0610063
dc.identifierhttp://arxiv.org/abs/cs/0610063
dc.identifierDans Rewriting Techniques and Applications, 10th International Conference, RTA-99 1631 (1999)
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/161661
dc.subjectLogic in Computer Science
dc.titleThe Calculus of Algebraic Constructions
dc.typetext

Files

Collections

arXiv