Sökning: "Leo Okawa Ericson"

Hittade 1 uppsats innehållade orden Leo Okawa Ericson.

  1. 1. Simple formally verified compiler in Lean

    Kandidat-uppsats, Uppsala universitet/Institutionen för informationsteknologi

    Författare :Leo Okawa Ericson; [2021]
    Nyckelord :;

    Sammanfattning : Computer checked proofs that a compiler is correct are important for increasing the confidence in programs. This report presents a simple compiler and a proof that the compiler is correct for terminating evaluations using the interactive theorem prover Lean, based on Concrete Semantics: with Isabelle/HOL. LÄS MER