Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 7 of 7 for “"Interactive theorem provers"”.
-
Interactive theorem provers: issues faced as a user and tackled as a developer
Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a …
-
Compiling Haskell into Lean: A Common Abstract Syntax for Haskell and Interactive Theorem Provers
… and executable Lean code that users can prove theorems about. We conducted a case study using a heap sort algorithm to support our claim that HS-TO-LEAN produces verifiable Lean code. Our approach is inspired by recent advances in formal verification of Haskell programs in Coq, and we currently …
-
Relational compilation: Functional-to-imperative code generation for performance-critical applications
Purely functional programs verified using interactive theorem provers typically need to be translated to run: either by extracting them to a similar language (like Coq to OCaml) or by proving them equivalent to deeply embedded implementations (like C programs). Traditionally, the first approach is …
-
Towards justifying computer algebra algorithms in Isabelle/HOL
As verification efforts using interactive theorem proving grow, we are in need of certified algorithms in computer algebra to tackle problems over the real numbers. This is important because uncertified procedures can drastically increase the size of the trust base and under- mine the overall …
-
User interaction widgets for interactive theorem proving
Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of …
-
A Tool for Producing Verified, Explainable Proofs
Mathematicians are reluctant to use interactive theorem provers. In this thesis I argue that this is because proof assistants don't emphasise explanations of proofs; and that in order to produce good explanations, the system must create proofs in a manner that mimics how humans would create proofs. …
-
Certifying homological algorithms to study biomedical images
En esta tesis se aborda el problema de la verificación de programas para el procesamiento homológico de imágenes biomédicas. Concretamente, se formalizan en la herramienta de demostración Coq/SSReflect algoritmos para el cálculo de grupos de homología, lo que produce programas ejecutables que son …