Normalising the associative law: An experiment with Martin-Löf's type theory
From MaRDI portal
Publication:809071
DOI10.1007/BF01245632zbMath0732.03023MaRDI QIDQ809071
Publication date: 1991
Published in: Formal Aspects of Computing (Search for Journal in Brave)
correctness; Martin-Löf's type theory; external logic; external program; inductively defined types; measure functions; normalizing semigroup expressions with respect to the associative law; proof checker ISABELLE; well-founded recursion
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
68N01: General topics in the theory of software
03F35: Second- and higher-order arithmetic and fragments
03-04: Software, source code, etc. for problems pertaining to mathematical logic and foundations
Related Items
Cites Work