Nuprl

The Nuprl system is a framework for reasoning about mathematics and programming. Over the years its design has been substantially improved to meet the demands of large-scale applications. Nuprl LPE, the newest release, features an open, distributed architecture centered around a flexible knowledge base and supports the cooperation of independent formal tools.


References in zbMATH (referenced in 394 articles , 5 standard articles )

Showing results 1 to 20 of 394.
Sorted by year (citations)

1 2 3 ... 18 19 20 next

  1. Bickford, Mark; Kozen, Dexter; Silva, Alexandra: Formalizing Moessner’s theorem and generalizations in \textscNuprl (2022)
  2. Angiuli, Carlo; Brunerie, Guillaume; Coquand, Thierry; Harper, Robert; Hou (Favonia), Kuen-Bang; Licata, Daniel R.: Syntax and models of Cartesian cubical type theory (2021)
  3. Berger, Ulrich; Tsuiki, Hideki: Intuitionistic fixed point logic (2021)
  4. Kohlhase, Michael; Rabe, Florian: Experiences from exporting major proof assistant libraries (2021)
  5. Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
  6. Cohen, Liron; Avron, Arnon: The middle ground-ancestral logic (2019)
  7. Johansson, Moa: Lemma discovery for induction. A survey (2019)
  8. Kellison, Ariel; Bickford, Mark; Constable, Robert: Implementing Euclid’s straightedge and compass constructions in type theory (2019)
  9. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
  10. Miller, Dale: Mechanized metatheory revisited (2019)
  11. Rahli, Vincent; Bickford, Mark; Cohen, Liron; Constable, Robert L.: Bar induction is compatible with constructive type theory (2019)
  12. Reynolds, Andrew; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark; Deters, Morgan: Refutation-based synthesis in SMT (2019)
  13. Angiuli, Carlo; Harper, Robert: Meaning explanations at higher dimension (2018)
  14. Avelar da Silva, Andréia B.; de Lima, Thaynara Arielly; Galdino, André Luiz: Formalizing ring theory in PVS (2018)
  15. Avron, Arnon; Cohen, Liron: Applicable mathematics in a minimal computational theory of sets (2018)
  16. Bickford, Mark; Cohen, Liron; Constable, Robert L.; Rahli, Vincent: Computability beyond Church-Turing via choice sequences (2018)
  17. Carette, Jacques; Farmer, William M.; Laskowski, Patrick: HOL Light QE (2018)
  18. Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
  19. Harper, Robert: Exception tracking in an open world (2018)
  20. Rahli, Vincent; Bickford, Mark: Validating Brouwer’s continuity principle for numbers using named exceptions (2018)

1 2 3 ... 18 19 20 next