The calculus of algebraic constructions

DOI10.1007/3-540-48685-2_25MaRDI QIDQ4938611zbMATH OpenFDO

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

Publication date 13 September 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48685-2_25

zbMATH Keywords

calculus of algebraic constructions

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Abstract data types; algebraic specification (68Q65)

Recommendations

• The calculus of constructions
• scientific article; zbMATH DE number 4069027
• Constructive algebra
• A course in constructive algebra
• Algebraic structures from calculus
• Calcular algebras
• CALCULUS IN ENVELOPING ALGEBRAS
• scientific article; zbMATH DE number 806913
• Constructive algebraic integration theory
• Constructing and Reconstructing of Algebras

Cited in

(25)

• A course in constructive algebra
• Abstract data type systems
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Corrigendum to: ``Inductive-data-type systems
• Constructive algebraic integration theory
• Normal higher-order termination
• scientific article; zbMATH DE number 4014064 (Why is no real title available?)
• scientific article; zbMATH DE number 4191621 (Why is no real title available?)
• scientific article; zbMATH DE number 7217919 (Why is no real title available?)
• Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• On lists and other abstract data types in the calculus of constructions
• Remarks on isomorphisms of simple inductive types
• scientific article; zbMATH DE number 1434122 (Why is no real title available?)
• Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
• Calcular algebras
• The calculus of dependent lambda eliminations
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• Inductively defined types in the Calculus of Constructions
• Types for Proofs and Programs
• Inductive-data-type systems
• The computability path order for beta-eta-normal higher-order rewriting
• An initial algebra approach to term rewriting systems with variable binders
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• A domain model characterising strong normalisation

This page was built for publication: The calculus of algebraic constructions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4938611)