Efficient Verified Programs in a Type Theory with Mixed Constructivity

DOI10.1093/LOGCOM/5.5.669zbMath0829.03015OpenAlexW2034260705MaRDI QIDQ4849649

James T. Sasaki

Publication date: 4 October 1995

Published in: Unnamed Author (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/5.5.669

zbMATH Keywords

constructive type theoryintuitionistic logicdenotational semanticstyped \(\lambda\)-calculusevidence semanticsprogramming logicmixed constructivityverified programming

Mathematics Subject Classification ID

Logic in computer science (03B70) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

This page was built for publication: Efficient Verified Programs in a Type Theory with Mixed Constructivity