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.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
- Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
- Anand, Abhishek; Rahli, Vincent: Towards a formally verified proof assistant (2014)
- Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: HOL with definitions: semantics, soundness, and a verified implementation (2014)
- Myreen, Magnus O.; Davis, Jared: The reflective milawa theorem prover is sound (down to the machine code that runs it) (2014)
- Myreen, Magnus O.; Owens, Scott; Kumar, Ramana: Steps towards verified implementations of HOL Light (2013)