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

DOI10.1007/BF01245632zbMATH Open0732.03023MaRDI QIDQ809071FDOQ809071

Authors: Michael Hedberg 

Publication date: 1991

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

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

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)

Cites Work

• Title not available (Why is that?)
• The calculus of constructions
• Do-it-yourself type theory
• Title not available (Why is that?)
• Terminating general recursion
• Comparing integrated and external logics of functional programs
• Proving termination of normalization functions for conditional expressions

Cited In (6)

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

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)