Formalizing Type Operations Using the “Image” Type Constructor

DOI10.1016/j.entcs.2006.05.041zbMath1262.03025OpenAlexW2096220787MaRDI QIDQ4917993

No author found.

Publication date: 3 May 2013

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2006.05.041

zbMATH Keywords

calculus of constructionstype theorytype constructor\texttt{Coq}\texttt{MetaPRL}\texttt{NuPRL}

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (2)

Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Exercising Nuprl’s Open-Endedness

Uses Software

• Coq
• MetaPRL
• Nuprl

Cites Work

• Theorem proving in higher order logics. 15th international conference, TPHOLs 2002, Hampton, VA, USA, August 20--23, 2002. Proceedings
• Do-it-yourself type theory
• Theorem proving in higher order logics. 16th international conference, TPHOLs 2003, Rome, Italy, September 8--12, 2003. Proceedings
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalizing Type Operations Using the “Image” Type Constructor