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.


References in zbMATH (referenced in 14 articles , 1 standard article )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
  2. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  3. Kunčar, Ondřej; Popescu, Andrei: A consistent foundation for Isabelle/HOL (2019)
  4. Moore, J. Strother: Milestones from the Pure Lisp Theorem Prover to ACL2 (2019)
  5. Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes: A verified generational garbage collector for CakeML (2019)
  6. 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)
  7. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
  8. Adams, Mark: HOL zero’s solutions for Pollack-inconsistency (2016)
  9. Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
  10. Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
  11. Anand, Abhishek; Rahli, Vincent: Towards a formally verified proof assistant (2014)
  12. Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: HOL with definitions: semantics, soundness, and a verified implementation (2014)
  13. Myreen, Magnus O.; Davis, Jared: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2014)
  14. Myreen, Magnus O.; Owens, Scott; Kumar, Ramana: Steps towards verified implementations of HOL Light (2013)