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

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, 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

• Coq
• 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