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 337 articles , 5 standard articles )

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

1 2 3 ... 15 16 17 next

  1. Dagand, Pierre-Evariste: The essence of ornaments (2017)
  2. Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian: Classification of alignments between concepts of formal mathematical systems (2017)
  3. Stump, Aaron: The calculus of dependent lambda eliminations (2017)
  4. Angiuli, Carlo; Morehouse, Edward; Licata, Daniel R.; Harper, Robert: Homotopical patch theory (2016)
  5. Bizjak, Aleš; Grathwohl, Hans Bugge; Clouston, Ranald; Møgelberg, Rasmus E.; Birkedal, Lars: Guarded dependent type theory with coinductive types (2016)
  6. Drăgoi, Cezara; Henzinger, Thomas A.; Zufferey, Damien: PSync: a partially synchronous language for fault-tolerant distributed algorithms (2016)
  7. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definitions in higher-order logic (2016)
  8. Lepigre, Rodolphe: A classical realizability model for a semantical value restriction (2016)
  9. Malecha, Gregory; Bengtson, Jesper: Extensible and efficient automation through reflective tactics (2016)
  10. Rabe, Florian: The future of logic: foundation-independence (2016)
  11. Rahli, Vincent: Exercising Nuprl’s open-endedness (2016)
  12. Schubert, Aleksy; Urzyczyn, Paweł; Walukiewicz-Chrząszcz, Daria: How hard is positive quantification? (2016)
  13. Anand, Abhishek; Rahli, Vincent: Towards a formally verified proof assistant (2014)
  14. Boy de la Tour, Thierry; Peltier, Nicolas: Analogy in automated deduction: a survey (2014)
  15. Constable, Robert; Bickford, Mark: Intuitionistic completeness of first-order logic (2014)
  16. Kaliszyk, Cezary; Rabe, Florian: Towards knowledge management for HOL Light (2014)
  17. Blazy, Sandrine (ed.); Paulin-Mohring, Christine (ed.); Pichardie, David (ed.): Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings (2013)
  18. Rahli, Vincent; Bickford, Mark; Anand, Abhishek: Formal program optimization in Nuprl using computational equivalence and partial types (2013)
  19. Armstrong, Alasdair; Foster, Simon; Struth, Georg: Dependently typed programming based on automated theorem proving (2012)
  20. Bove, Ana; Dybjer, Peter; Sicard-Ramírez, Andrés: Combining interactive and automatic reasoning in first order theories of functional programs (2012)

1 2 3 ... 15 16 17 next