Sökning: "Oskar Abrahamsson"

Hittade 2 avhandlingar innehållade orden Oskar Abrahamsson.

1. 1. A Verified Theorem Prover for Higher-Order Logic

   Författare :Oskar Abrahamsson; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; formal verification; higher-order logic; interactive theorem provers;

   Sammanfattning : This thesis is about mechanically establishing the correctness of computer programs. In particular, we are interested in establishing the correctness of tools used in computer-aided mathematics. We build on tools for proof-producing program synthesis, and verified compilation, and a verified theorem proving kernel. LÄS MER

3. 2. Verified proof checking for higher-order logic

   Författare :Oskar Abrahamsson; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES;

   Sammanfattning : This thesis is about verified computer-aided checking of mathematical proofs. We build on tools for proof-producing program synthesis, and verified compilation, and a verified theorem proving kernel. Using these tools, we have produced a mechanized proof checker for higher-order logic that is verified to only accept valid proofs. LÄS MER