Jitawa

swMATH12812MaRDI QIDQ24736FDOQ24736

Author name not available (Why is that?)

Official website: http://www.cl.cam.ac.uk/~mom22/jitawa/

Described by source

• The reflective Milawa theorem prover is sound (down to the machine code that runs it)

Cited In (33)

• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Aligning concepts across proof assistant libraries
• A verified generational garbage collector for CakeML
• Formalization of the resolution calculus for first-order logic
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Steps towards Verified Implementations of HOL Light
• A verified proof checker for higher-order logic
• ProofPower
• Polar
• CompCertTSO
• CakeML
• Milawa
• HOL Zero
• HOL Zero's solutions for Pollack-inconsistency
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• theoremprover-museum
• GCminor
• Abstract Soundness
• Knuth Bendix Orders
• Incompleteness Theorems
• Incredible Proof Machine
• Light-weight Containers
• Verified Prover
• FOL_Harrison
• DefunT
• OpenTheory
• TXDT
• Towards a formally verified proof assistant
• HOL with definitions: semantics, soundness, and a verified implementation
• Milestones from the Pure Lisp Theorem Prover to ACL2
• Metamath Zero
• A formalization and proof checker for Isabelle's metalogic
• A consistent foundation for Isabelle/HOL

This page was built for software: Jitawa