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

DOI10.1007/BF01245632zbMath0732.03023MaRDI QIDQ809071

Michael Hedberg

Publication date: 1991

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

zbMATH Keywords

correctnessMartin-Löf's type theoryexternal logicexternal programinductively defined typesmeasure functionsnormalizing semigroup expressions with respect to the associative lawproof checker ISABELLEwell-founded recursion

Mathematics Subject Classification ID

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

Related Items (3)

Inductive families ⋮ A type theoretic interpretation of constructive domain theory ⋮ Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids

Cites Work

• Do-it-yourself type theory
• Comparing integrated and external logics of functional programs
• Proving termination of normalization functions for conditional expressions
• The calculus of constructions
• Terminating general recursion
• Unnamed Item
• Unnamed Item

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