Innovations in computational type theory using Nuprl

DOI10.1016/J.JAL.2005.10.005zbMath1107.68090OpenAlexW1977189131WikidataQ56228326 ScholiaQ56228326MaRDI QIDQ865639

L. Lorigo, R. Eaton, E. Moran, S. F. Allen, Christoph Kreitz, Mark Bickford, Robert L. Constable

Publication date: 20 February 2007

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

Full work available at URL: https://doi.org/10.1016/j.jal.2005.10.005

zbMATH Keywords

program extractionMartin-Löf type theorytacticscomputational type theorydependent intersection typesformal digital librarieslogic of eventspolymorphic subtypingproofs as programsunion types

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (17)

A language with type-dependent equality ⋮ The effects of effects on constructivism ⋮ Implementing Euclid's straightedge and compass constructions in type theory ⋮ Monotone recursive types and recursive data representations in Cedille ⋮ Intuitionistic completeness of first-order logic ⋮ Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language ⋮ Tactics for hierarchical proof ⋮ Unnamed Item ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Impredicative encodings of inductive-inductive data in Cedille ⋮ \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity ⋮ Cartesian cubical computational type theory: Constructive reasoning with paths and equalities ⋮ Exercising Nuprl’s Open-Endedness ⋮ Nuprl ⋮ Manifest Fields and Module Mechanisms in Intensional Type Theory ⋮ Building Mathematics-Based Software Systems to Advance Science and Create Knowledge ⋮ Formally computing with the non-computable

Uses Software

• Unnamed Item
• PVS
• MetaPRL
• Automath
• OMDoc
• LCF
• JProver
• MathWeb
• Horus

Cites Work

• Intuitionistic completeness of first-order logic
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Combinatory logic. With two sections by William Craig.
• An introduction to the PL/CV2 programming logic
• Constructivism in mathematics. An introduction. Volume II
• Theorem proving in higher order logics. 16th international conference, TPHOLs 2003, Rome, Italy, September 8--12, 2003. Proceedings
• Edinburgh LCF. A mechanized logic of computation
• Mathematical knowledge management in HELM
• Writing programs that construct proofs
• A uniform procedure for converting matrix proofs into sequent-style systems
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Emergence of Scaling in Random Networks
• Constructive mathematics and computer programming
• The Type Theory of PL/CV3
• Data Types as Lattices
• Time, clocks, and the ordering of events in a distributed system
• Building reliable, high-performance networks with the Nuprl proof development system
• Exploring abstract algebra in constructive type theory
• Hybrid interactive theorem proving using nuprl and HOL
• Mathematical Knowledge Management
• Foundations for the implementation of higher-order subtyping
• The mutual exclusion problem
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Innovations in computational type theory using Nuprl