Jitawa
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 14 articles , 1 standard article )
Showing results 1 to 14 of 14.
Sorted by year (- Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
- Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
- Kunčar, Ondřej; Popescu, Andrei: A consistent foundation for Isabelle/HOL (2019)
- Moore, J. Strother: Milestones from the Pure Lisp Theorem Prover to ACL2 (2019)
- Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes: A verified generational garbage collector for CakeML (2019)
- Zakowski, Yannick; Cachera, David; Demange, Delphine; Petri, Gustavo; Pichardie, David; Jagannathan, Suresh; Vitek, Jan: Verifying a concurrent garbage collector with a rely-guarantee methodology (2019)
- Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
- Adams, Mark: HOL zero’s solutions for Pollack-inconsistency (2016)
- 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)