Foundations of software

CS-452

Livecoding Progress and Preservation Arith

This page is part of the content downloaded from Livecoding Progress and Preservation Arith on Monday, 30 June 2025, 16:54. Note that some content and any files larger than 50 MB are not downloaded.

Page content

We defined a typesystem for the Arith language and then we proved progress and preservation.

https://gitlab.epfl.ch/fos/ArithProgressAndPreservation/-/blob/main/Fos/SmallStep.lean?ref_type=heads