Unifying sets and programs via dependent types

DOI10.1016/j.apal.2011.09.016zbMath1238.68050OpenAlexW2070864670MaRDI QIDQ408534

Wojciech Moczydłowski

Publication date: 10 April 2012

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2011.09.016

zbMATH Keywords

proof theoryconstructive set theorydependent type theory

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
• Nuprl
• LEGO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Lectures on the Curry-Howard isomorphism
• Higher-order rewrite systems and their confluence
• Map theory
• Light affine set theory: A naive set theory of polynomial time
• Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
• A framework for defining logics
• The B-Book
• Term Rewriting and All That
• On the Cauchy Completeness of the Constructive Cauchy Reals
• A Normalizing Intuitionistic Set Theory with Inaccessible Sets
• Normalization of IZF with Replacement

This page was built for publication: Unifying sets and programs via dependent types