guru is a programming language created in 2009. OpTT has been implemented in the GURU verified programming language, which includes a type- and proof-checker, and a compiler to efficient C code. In addition to the core OpTT, GURU implements a number of extensions, including ones for verification of programs using mutable state and input/output. This paper gives an introduction to verified programming in GURU.

11Years Old ?Users ?Jobs
  • guru first appeared in 2009
  • Have a question about guru not answered here? Email me and let me know how I can help.

Example code from the web:

Inductive trie : Fun(A:type).type :=
trie_none : Fun(A:type).<trie A>
| trie_exact : Fun(A:type)(s:string)(a:A).<trie A>
| trie_next : Fun(A:type)(o:<option A>)
(unique l:<charvec <trie A>>).
<trie A>.

Last updated June 22nd, 2020

Edit guru on GitHub