Title: Reading between the lines in constructive type theory
Abstract: We formulate and investigate various ways of (conservatively) extending Martin-Löf's type theories with separation types and choice principles and demonstrate how these extenstions can be employed to formalize Bishop's mathematical practice of hiding and recovering witnessing information.
Publication Year: 1997
Publication Date: 1997-04-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 1
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot