Search for dissertations about: "higher-order logic HOL"

Found 3 swedish dissertations containing the words higher-order logic HOL.

2. 1. Conservative Definitions for Higher-order Logic with Ad-hoc Overloading

   Author : Arve Gengelbach; Tjark Weber; Joachim Parrow; Andrei Popescu; Uppsala universitet; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES; higher-order logic HOL ; conservative extension; ad-hoc overloading; definitions; Computer Science; Datavetenskap;

   Abstract : With an ever growing dependency on computer systems, the need to guarantee their correct behaviour increases. Mathematically rigorous techniques like formal verification offer a way to derive a system's mathematical properties for example with the help of a theorem prover. READ MORE

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

   Author : Oskar Abrahamsson; Chalmers tekniska högskola; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES;

   Abstract : 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. READ MORE

5. 3. A transformational approach to formal digital system design

   Author : Mats Larsson; Linköpings universitet; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES;

   Abstract : The continuing development in electronic technology has made it possible to fit more and more functionality on a single chip, thus allowing digital systems to become increasingly complex. This has led to a need for better synthesis and verification methods and tools to manage this complexity.Formal digital system design is one such method. READ MORE