Unifying sets and programs via dependent types

DOI10.1016/J.APAL.2011.09.016MaRDI QIDQ408534zbMATHOpenAlexFDO

Authors 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

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

Recommendations

• Unifying Sets and Programs via Dependent Types
• scientific article; zbMATH DE number 1678369
• Combining Type Theory and Untyped Set Theory
• Higher-order unification with dependent function types
• Combining proofs and programs in a dependently typed language

Cites work

• scientific article; zbMATH DE number 3427309 (Why is no real title available?)
• scientific article; zbMATH DE number 4012604 (Why is no real title available?)
• scientific article; zbMATH DE number 3664922 (Why is no real title available?)
• scientific article; zbMATH DE number 1062123 (Why is no real title available?)
• scientific article; zbMATH DE number 1070622 (Why is no real title available?)
• scientific article; zbMATH DE number 1479608 (Why is no real title available?)
• scientific article; zbMATH DE number 1552509 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A Normalizing Intuitionistic Set Theory with Inaccessible Sets
• A framework for defining logics
• Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
• Higher-order rewrite systems and their confluence
• Lectures on the Curry-Howard isomorphism
• Light affine set theory: A naive set theory of polynomial time
• Map theory
• Normalization of IZF with Replacement
• On the Cauchy completeness of the constructive Cauchy reals
• Term Rewriting and All That
• The B-Book
• Types and programing languages

Cited in

(3)

• scientific article; zbMATH DE number 2111733 (Why is no real title available?)
• Unifying Sets and Programs via Dependent Types
• scientific article; zbMATH DE number 1678369 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq
• ML
• HOL
• Nuprl
• LEGO

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q408534)