The calculus of algebraic constructions

Frédéric Blanqui; Jean Pierre Jouannaud; Mitsuhiro Okada

doi:10.1007/3-540-48685-2_25

The calculus of algebraic constructions

Frédéric Blanqui, Jean Pierre Jouannaud, Mitsuhiro Okada

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

37 Citations (Scopus)

Abstract

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 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. Full proofs are available at http://www.lri.fr/~blanqui/publis/rta99full.ps.gz.

Original language	English
Title of host publication	Rewriting Techniques and Applications - 10th International Conference, RTA 1999, Proceedings
Editors	Paliath Narendran, Michael Rusinowitch
Publisher	Springer Verlag
Pages	301-316
Number of pages	16
ISBN (Print)	3540662014, 9783540662013
DOIs	https://doi.org/10.1007/3-540-48685-2_25
Publication status	Published - 1999
Externally published	Yes
Event	10th International Conference on Rewriting Techniques and Applications, RTA 1999 - Trento, Italy Duration: 1999 Jul 2 → 1999 Jul 4

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1631
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	10th International Conference on Rewriting Techniques and Applications, RTA 1999
Country/Territory	Italy
City	Trento
Period	99/7/2 → 99/7/4

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/3-540-48685-2_25

Cite this

Blanqui, F., Jouannaud, J. P., & Okada, M. (1999). The calculus of algebraic constructions. In P. Narendran, & M. Rusinowitch (Eds.), Rewriting Techniques and Applications - 10th International Conference, RTA 1999, Proceedings (pp. 301-316). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1631). Springer Verlag. https://doi.org/10.1007/3-540-48685-2_25

The calculus of algebraic constructions. / Blanqui, Frédéric; Jouannaud, Jean Pierre; Okada, Mitsuhiro.
Rewriting Techniques and Applications - 10th International Conference, RTA 1999, Proceedings. ed. / Paliath Narendran; Michael Rusinowitch. Springer Verlag, 1999. p. 301-316 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1631).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Blanqui, F, Jouannaud, JP & Okada, M 1999, The calculus of algebraic constructions. in P Narendran & M Rusinowitch (eds), Rewriting Techniques and Applications - 10th International Conference, RTA 1999, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1631, Springer Verlag, pp. 301-316, 10th International Conference on Rewriting Techniques and Applications, RTA 1999, Trento, Italy, 99/7/2. https://doi.org/10.1007/3-540-48685-2_25

Blanqui F, Jouannaud JP, Okada M. The calculus of algebraic constructions. In Narendran P, Rusinowitch M, editors, Rewriting Techniques and Applications - 10th International Conference, RTA 1999, Proceedings. Springer Verlag. 1999. p. 301-316. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-48685-2_25

Blanqui, Frédéric ; Jouannaud, Jean Pierre ; Okada, Mitsuhiro. / The calculus of algebraic constructions. Rewriting Techniques and Applications - 10th International Conference, RTA 1999, Proceedings. editor / Paliath Narendran ; Michael Rusinowitch. Springer Verlag, 1999. pp. 301-316 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{e93410d06b5143c5990c31d55f4c8ee0,

title = "The calculus of algebraic constructions",

abstract = "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 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. Full proofs are available at http://www.lri.fr/~blanqui/publis/rta99full.ps.gz.",

author = "Fr{\'e}d{\'e}ric Blanqui and Jouannaud, {Jean Pierre} and Mitsuhiro Okada",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1999.; 10th International Conference on Rewriting Techniques and Applications, RTA 1999 ; Conference date: 02-07-1999 Through 04-07-1999",

year = "1999",

doi = "10.1007/3-540-48685-2_25",

language = "English",

isbn = "3540662014",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "301--316",

editor = "Paliath Narendran and Michael Rusinowitch",

booktitle = "Rewriting Techniques and Applications - 10th International Conference, RTA 1999, Proceedings",

}

TY - GEN

T1 - The calculus of algebraic constructions

AU - Blanqui, Frédéric

AU - Jouannaud, Jean Pierre

AU - Okada, Mitsuhiro

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1999.

PY - 1999

Y1 - 1999

N2 - 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 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. Full proofs are available at http://www.lri.fr/~blanqui/publis/rta99full.ps.gz.

AB - 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 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. Full proofs are available at http://www.lri.fr/~blanqui/publis/rta99full.ps.gz.

UR - http://www.scopus.com/inward/record.url?scp=84957655853&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84957655853&partnerID=8YFLogxK

U2 - 10.1007/3-540-48685-2_25

DO - 10.1007/3-540-48685-2_25

M3 - Conference contribution

AN - SCOPUS:84957655853

SN - 3540662014

SN - 9783540662013

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 301

EP - 316

BT - Rewriting Techniques and Applications - 10th International Conference, RTA 1999, Proceedings

A2 - Narendran, Paliath

A2 - Rusinowitch, Michael

PB - Springer Verlag

T2 - 10th International Conference on Rewriting Techniques and Applications, RTA 1999

Y2 - 2 July 1999 through 4 July 1999

ER -

The calculus of algebraic constructions

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this