Proof normalization of structured algebraic specifications is convergent

DOI10.1007/3-540-48483-3_21MaRDI QIDQ4941939zbMATH OpenFDO

Authors John N. Crossley, Hannes Peterreins, Martin Wirsing

Publication date 25 October 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-48483-3_21

zbMATH Keywords

completenesscut eliminationnatural deduction calculusproof term reductionsproof transformationssoundnessstructured algebraic specifications

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Abstract data types; algebraic specification (68Q65)

Recommendations

• Proof systems for structured algebraic specifications: An overview
• Proof systems for structured specifications and their refinements
• Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved
• A relatively complete calculus for structured heterogeneous specifications
• Some general results about proof normalization

Cited in

(3)

• On normal forms for structured specifications with generating constraints
• scientific article; zbMATH DE number 995878 (Why is no real title available?)
• Proof systems for structured algebraic specifications: An overview

This page was built for publication: Proof normalization of structured algebraic specifications is convergent

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