×

Jitawa

swMATH ID: 12812
Software Authors: Myreen, M.O., Davis, J.
Description: Jitawa — a verified Lisp runtime for Milawa. This page contains source code, documentation and proofs scripts relating to a verified Lisp runtime, called Jitawa. Jitawa was designed to host Jared Davis’ Milawa theorem prover — a prover which we have formally proved to be sound when run on Jitawa.
Homepage: http://www.cl.cam.ac.uk/~mom22/jitawa/
Dependencies: Milawa
Related Software: Milawa; HOL; HOL Light; Coq; Isabelle/HOL; CakeML; Isabelle; OpenTheory; LCF; ML; HOL Zero; ProofPower; ACL2; NQTHM; z3; Agda; Mizar; Isar; Completeness theorem; MLton
Referenced in: 14 Publications

Referencing Publications by Year