LoreonLabsPlatform

Overview

Intelligence

Markets
Builders
Research
Ecosystems
Launchpads

Search

HTML

hoare_wlp_fstar

esteffin/hoare_wlp_fstar

HTMLEmerging

Stars

1

Forks

—

Contributors

2

Last push

136mo ago

Recent commits

Latest commits.

Apache license
de947f4Catalin Hritcu136mo ago
Merge branch 'master' of https://github.com/esteffin/hoare_wlp_fstar
f665c47Simon Forest137mo ago
wlp_weakest' proof complete. By the way, I needed to write while5' at some point and it
7e01f9bSimon Forest137mo ago
A "diagram" from the project presentation
cd50919Catalin Hritcu137mo ago
most of impl_wlp written. There is still the while case to write (this is going to be painful …), and after we are done.
0487818Simon Forest137mo ago

Fixed while case + formatting

b711281Catalin Hritcu137mo ago

Merge branch 'master' of https://github.com/esteffin/hoare_wlp_fstar

aa16e10Simon Forest137mo ago

Version with most of the syntactic version of hoare logic. Still a typechecking error for the While case …

a553345Simon Forest137mo ago

Top contributors

Builders behind this project.