*** This version of Confluence is for testing only and contains a copy of content from June 29th 2026. No changes will be preserved. ***
...
The main tool we use is EventML which is a programming and specification language. EventML, built by Vinvent Vincent Rahli, cooperates with the Nuprl interactive theorem prover at every stage of program development to help programmers ensure correctness, document the code, and support modifications and improvements. It generates an Inductive Logical Form that proves the specification and can also automatically synthesize code.
...