Singleton, union, and intersection types for program extraction
From MaRDI portal
Publication:1322477
DOI10.1006/inco.1994.1016zbMath0804.68091MaRDI QIDQ1322477
Publication date: 5 May 1994
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/inco.1994.1016
lambda calculus; type theory; Curry-Howard isomorphism; refinement types; specifications of programs
68N15: Theory of programming languages
68Q60: Specification and verification (program logics, model checking, etc.)
03B40: Combinatory logic and lambda calculus
Related Items
Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models, \(QPC_ 2\): A constructive calculus with parameterized specifications, Intersection and singleton type assignment characterizing finite Böhm-trees, Manifest Fields and Module Mechanisms in Intensional Type Theory
Uses Software