Unifying sets and programs via dependent types

DOI10.1016/J.APAL.2011.09.016zbMATH Open1238.68050OpenAlexW2070864670MaRDI QIDQ408534FDOQ408534

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

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

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)

Cites Work

• Title not available (Why is that?)
• A framework for defining logics
• Lectures on the Curry-Howard isomorphism
• The B-Book
• Term Rewriting and All That
• Title not available (Why is that?)
• Title not available (Why is that?)
• Types and programing languages
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the Cauchy Completeness of the Constructive Cauchy Reals
• A Normalizing Intuitionistic Set Theory with Inaccessible Sets
• Normalization of IZF with Replacement

Cited In (3)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Unifying Sets and Programs via Dependent Types

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)