Unifying Sets and Programs via Dependent Types

DOI10.1007/978-3-540-92687-0_25zbMath1211.68097OpenAlexW1507092030MaRDI QIDQ3605541

Wojciech Moczydłowski

Publication date: 24 February 2009

Published in: Logical Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-92687-0_25

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Metamathematics of constructive systems (03F50)

Uses Software

• Coq
• ML
• HOL
• LEGO

Cites Work

• Lectures on the Curry-Howard isomorphism
• Map theory
• Light affine set theory: A naive set theory of polynomial time
• Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
• The B-Book
• On the Cauchy Completeness of the Constructive Cauchy Reals
• A Normalizing Intuitionistic Set Theory with Inaccessible Sets
• Normalization of IZF with Replacement
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Unifying Sets and Programs via Dependent Types