Singleton, union, and intersection types for program extraction

DOI10.1006/inco.1994.1016zbMath0804.68091OpenAlexW2116636571MaRDI QIDQ1322477

Susumu Hayashi

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

zbMATH Keywords

lambda calculustype theoryCurry-Howard isomorphismrefinement typesspecifications of programs

Mathematics Subject Classification ID

Related Items (5)

Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models ⋮ Manifest Fields and Module Mechanisms in Intensional Type Theory ⋮ Intersection and singleton type assignment characterizing finite Böhm-trees ⋮ Lightweight Static Capabilities ⋮ \(QPC_ 2\): A constructive calculus with parameterized specifications

Uses Software

• Coq

This page was built for publication: Singleton, union, and intersection types for program extraction