System ST toward a type system for extraction and proofs of programs
From MaRDI portal
Publication:1400600
DOI10.1016/S0168-0072(03)00002-2zbMath1030.03014MaRDI QIDQ1400600
Publication date: 13 August 2003
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The system \({\mathcal F}\) of variable types, fifteen years later
- Polymorphic type inference and containment
- Recursive programming with proofs
- Positive subtyping
- Strong Normalization with Singleton Types
- A new type assignment for λ-terms
- Pruning simply typed -terms
- Deciding type equivalence in a language with singleton kinds
- An axiomatic basis for computer programming
- Studies of a theory of specifications with built-in program extraction