On specifications, subset types and interpretation of proposition in type theory

DOI10.1007/BF01995110zbMath0788.68095MaRDI QIDQ688736

Anne Salvesen

Publication date: 2 June 1994

Published in: BIT (Search for Journal in Brave)

zbMATH Keywords

verificationprogramming languagespecification languagetype theoryprogram synthesisGödel formulasprogramming logic

Mathematics Subject Classification ID

Related Items (1)

Realist Consequence, Epistemic Inference, Computational Correctness

Uses Software

• Nuprl

Cites Work

• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On specifications, subset types and interpretation of proposition in type theory