Some normalization properties of martin-löf's type theory, and applications

DOI10.1007/3-540-54415-1_60zbMath1493.68099OpenAlexW2110543549MaRDI QIDQ5096234

Douglas J. Howe, David A. Basin

Publication date: 16 August 2022

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-54415-1_60

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Metamathematics of constructive systems (03F50) Type theory (03B38)

Cites Work

• A framework for defining logics
• Natural deduction as higher-order resolution
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item