Singleton, union and intersection types for program extraction

DOI10.1007/3-540-54415-1_71zbMath1494.68059OpenAlexW4243877942MaRDI QIDQ5096245

Susumu Hayashi

Publication date: 16 August 2022

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-54415-1_71

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40) Type theory (03B38)

Related Items (2)

Logic of refinement types ⋮ Programming with streams in Coq a case study: The Sieve of Eratosthenes

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The semantics of second-order lambda calculus
• The calculus of constructions
• Recursive programming with proofs
• Typing and computational properties of lambda expressions
• Intersection and union types: Syntax and semantics
• An ideal model for recursive polymorphic types
• Introduction to generalized type systems

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