swMATH6751WikidataQ22907407 ScholiaQ22907407MaRDI QIDQ18826FDOQ18826
Author name not available (Why is that?)
Official website: http://www.nuprl.org/
Cited In (only showing first 100 items - show all)
- User interaction with the Matita proof assistant
- Functional and Logic Programming
- Mechanical Verification of a Constructive Proof for FLP
- The Twelf Proof Assistant
- Automath and Pure Type Systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- APS-1
- Theorema
- ML
- TPS
- MAYA
- MetaPRL
- Mizar
- IsaWin
- Isabelle/ZF
- Miranda
- TAS
- HOL
- TeXmacs
- CIRC
- Matita
- ETPS
- AEtnaNova
- Ivor
- Prolog
- HOL Light
- HOL-Omega
- SATCHMO
- C-CoRN
- 2OBJ
- Automath
- MMT
- Twelf
- OMDoc
- QMT
- Plastic
- NQTHM
- MMT
- AURA
- Title not available (Why is that?)
- LCF
- ALF
- MBase
- IMPS
- Alfalfa
- Camlflow
- iTasks
- Agda
- gaia
- Cayenne
- Epigram
- AoPA
- Irdis
- LEGO
- Mella
- evt
- K-Maude
- Minlog
- CtCoq
- SCC
- JProver
- PhoX
- MathWeb
- Analytica
- PROSPER
- PITP
- Specware
- FoCaLiZe
- ModLeanTAP
- Referee
- Roo
- HOT
- dedukti
- VeriML
- Mezzo
- HoTT
- Lean
- UniMath
- CoALP
- Distal
- Mathematical Knowledge Management
- FreshML
- OMEGA
- HOL Light QE
- CLAM
- HOL90
- InKa
- Leo
- Lambda-Clam
- MKRP
- Omega-ANTS
- Waldmeister
- XBarnacle
- TPS: A hybrid automatic-interactive system for developing proofs
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- IMPS: An interactive mathematical proof system
- An overview of the Tecton proof system
- FoCaLiZe and Dedukti to the rescue for proof interoperability
- Fixpoints and search in PVS
This page was built for software: Nuprl
