Normalising the associative law: An experiment with Martin-Löf's type theory

DOI10.1007/BF01245632MaRDI QIDQ809071zbMATH OpenFDO

Authors Michael Hedberg

Publication date 1991

Published in Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

correctnessexternal logicexternal programinductively defined typesmeasure functionsnormalizing semigroup expressions with respect to the associative lawproof checker ISABELLEwell-founded recursionMartin-Löf's type theory

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Second- and higher-order arithmetic and fragments (03F35) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Recommendations

• Some normalization properties of Martin-Löf's type theory, and applications
• Program derivation in type theory: A partitioning problem
• Per Martin-Löf's type theory for automated program writing
• Comparing integrated and external logics of functional programs
• Derivation of a parsing algorithm in Martin-Löf's theory of types

Cites work

• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• Comparing integrated and external logics of functional programs
• Do-it-yourself type theory
• Proving termination of normalization functions for conditional expressions
• Terminating general recursion
• The calculus of constructions

Cited in

(7)

• Extension of the formal system of the theory of expressions with arities and its strong normalization property
• A type theoretic interpretation of constructive domain theory
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Some normalization properties of Martin-Löf's type theory, and applications
• Inductive families
• Comparing integrated and external logics of functional programs
• Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids

This page was built for publication: Normalising the associative law: An experiment with Martin-Löf's type theory

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