- Referenced in 390 articles
- Nuprl system is a framework for reasoning about mathematics and programming. Over the years ... meet the demands of large-scale applications. Nuprl LPE, the newest release, features an open...
- Referenced in 406 articles
- which the better known current ones are Nuprl...
- Referenced in 191 articles
- dependent types, such as Coq, Epigram and NuPRL. This package includes both a command-line...
- Referenced in 39 articles
- proof editor closely based on the Cornell NuPRL system, but implemented in Prolog. CLAM...
- Referenced in 13 articles
- proof objects, and its integration into the Nuprl proof development system...
- Referenced in 1 article
- Nuprl-Light: an implementation framework for higher-order logics. this paper we describe Nuprl-Light ... descendent of the Nuprl  theorem prover, that addresses the issues of diversity and sharing ... call it an implementation framework. Instead, Nuprl-Light provides a meta-framework where logical frameworks ... such as LF, Nuprl, set theory, and other theories can be defined and developed. Since...
- Referenced in 2 articles
- cubical computational type theory, which extends the Nuprl semantics by higher-dimensional features inspired...
- Referenced in 172 articles
- Axiom is a general purpose Computer Algebra system...
- Referenced in 1818 articles
- Coq is a formal proof management system. It...
- Referenced in 66 articles
- Dafny is an imperative object-based language with...
- Referenced in 5 articles
- The science and engineering disciplines rely heavily on...
- Referenced in 624 articles
- PVS is a verification system: that is, a...
- Referenced in 290 articles
- Eiffel is an ISO-standardized, object-oriented programming...
- Referenced in 41 articles
- KeYmaera: A hybrid theorem prover for hybrid systems...
- Referenced in 26 articles
- MetaPRL is two things: it is a logical...
- Referenced in 514 articles
- Higher Order Logic (HOL) is a programming environment...
- Referenced in 157 articles
- Edinburgh LCF. A mechanized logic of computation. From...
- Referenced in 46 articles
- Cakeml, a verified implementation of ML. We have...
- Referenced in 107 articles
- LEGO is an interactive proof development system (proof...