The calculus of algebraic constructions

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

32 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 languageEnglish
Title of host publicationRewriting Techniques and Applications - 10th International Conference, RTA 1999, Proceedings
EditorsPaliath Narendran, Michael Rusinowitch
PublisherSpringer Verlag
Pages301-316
Number of pages16
ISBN (Print)3540662014, 9783540662013
DOIs
Publication statusPublished - 1999
Event10th International Conference on Rewriting Techniques and Applications, RTA 1999 - Trento, Italy
Duration: 1999 Jul 21999 Jul 4

Publication series

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

Other

Other10th International Conference on Rewriting Techniques and Applications, RTA 1999
CountryItaly
CityTrento
Period99/7/299/7/4

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'The calculus of algebraic constructions'. Together they form a unique fingerprint.

Cite this