Skip to main content

Browse the archive

Revision 93912f6d687ecad2258fd22f576776ed2d2e59a7 authored by Raphaël Cauderlier on 21 December 2019, 22:12:06 UTC, committed by Raphaël Cauderlier on 14 May 2020, 19:39:36 UTC 
[michocoq] Prove second half of typer correctness
 
This completes the correctness proof of the typer in Optimized
mode. Before this, only the typed -> untyped -> typed round-trip was
certified.
1 parent daec052
Raw File
coq-mi-cho-coq.install 
bin: [
  "src/michocoq/extraction/_build/michocoq.native" {"michocoq"}
]
back to top