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

DOI10.1007/BF01995110MaRDI QIDQ688736zbMATH OpenFDO

Authors Anne Salvesen

Publication date 2 June 1994

Published in BIT (Search for Journal in Brave)

zbMATH Keywords

verificationprogramming languagetype theoryspecification languageprogram synthesis[https://portal.mardi4nfdi.de/w/index.php?title=+Special%3ASearch&search=G%EF%BF%BD%EF%BF%BDdel+formulas&go=Go G��del formulas]programming logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Propositions and specifications of programs in Martin-Löf's type theory
• On specifications, theories, and models with higher types
• Subtyping and intersection types revisited
• Publication:4944846
• On type inference in the intersection type discipline
• Semantic subtyping, dealing set-theoretically with function, union, intersection, and negation types
• La théorie intuitionniste des types : sémantique des preuves et théorie des constructions
• Intersection types from a proof-theoretic perspective
• scientific article; zbMATH DE number 1302061
• A Theory of Ambiguous Types and Its Axiomatizations

Cites work

• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3360145 (Why is no real title available?)
• Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard

Cited in

(4)

• Realist consequence, epistemic inference, computational correctness
• Propositional forms of judgemental interpretations
• scientific article; zbMATH DE number 517090 (Why is no real title available?)
• Classical predicative logic-enriched type theories

Describes a project that uses

Uses Software

• Nuprl

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q688736)