Reading between the lines in constructive type theory

DOI10.1093/logcom/7.2.229zbMath0882.03058OpenAlexW2117463039MaRDI QIDQ4340420

Raymond Turner

Publication date: 10 June 1997

Published in: Journal of Logic and Computation (Search for Journal in Brave)

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

zbMATH Keywords

Bishop's constructive mathematicsexact real arithmeticchoice principlesMartin-Löf's type theoriesseparation typessuppressing and recovering witnessing information

Mathematics Subject Classification ID

Logic in computer science (03B70) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Related Items (1)

MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK

Uses Software

• Nuprl

This page was built for publication: Reading between the lines in constructive type theory