| 1. |
- Abrahamsson, Oskar, 1986
(författare)
-
A verified proof checker for higher-order logic
- 2020
-
Ingår i: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 112
-
Tidskriftsartikel (refereegranskat)abstract
- We present a computer program for checking proofs in higher-order logic (HOL) that is verified to accept only valid proofs. The proof checker is defined as functions in HOL and synthesized to CakeML code, and uses the Candle theorem prover kernel to check logical inferences. The checker reads proofs in the OpenTheory article format, which means proofs produced by various HOL proof assistants are supported. The proof checker is implemented and verified using the HOL4 theorem prover, and comes with a proof of soundness. (C) 2020 Elsevier Inc. All rights reserved.
|
|
| 2. |
- Abrahamsson, Oskar, 1986
(författare)
-
A Verified Theorem Prover for Higher-Order Logic
- 2022
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- 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. With these, we have produced an interactive theorem prover for higher-order logic, called Candle, that is verified to accept only true theorems. To the best of our knowledge, Candle is the only interactive theorem prover for higher-order logic that has been verified to this degree. Candle and all technology that underpins it is developed using the HOL4 theorem prover. We use proof-producing synthesis and the verified CakeML compiler to obtain a machine code executable for the Candle theorem prover. Because the CakeML compiler is verified to preserve program semantics, we are able to obtain a soundness result about the machine code which implements the Candle theorem prover.
|
|
| 3. |
- Abrahamsson, Oskar, 1986, et al.
(författare)
-
Automatically introducing tail recursion in CakeML
- 2018
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 10788, s. 118-134
-
Konferensbidrag (refereegranskat)abstract
- We describe and implement an optimizing compiler transformation which turns non–tail-recursive functions into equivalent tail-recursive functions in an intermediate language of the CakeML compiler. CakeML is a strongly typed functional language based on Standard ML with call-by-value semantics and a fully verified compiler. We integrate our implementation into CakeML compiler, and provide a machine-checked proof verifying that the observational semantics of programs is preserved under the transformation. To the best of our knowledge, this is the first fully verified implementation of this transformation in any modern compiler. Moreover, our verification efforts uncover surprising drawbacks in some of the verification techniques employed in several parts of the CakeML compiler. We provide a work-around for these drawbacks, and compare it to potential alternatives.
|
|
| 4. |
- Abrahamsson, Oskar, 1986, et al.
(författare)
-
Candle: A Verified Implementation of HOL Light
- 2022
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. ; 237
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a fully verified interactive theorem prover for higher-order logic, more specifically: a fully verified clone of HOL Light. Our verification proof of this new system results in an end-to-end correctness theorem that guarantees the soundness of the entire system down to the machine code that executes at runtime. Our theorem states that every exported fact produced by this machine-code program is valid in higher-order logic. Our implementation consists of a read-eval-print loop (REPL) that executes the CakeML compiler internally. Throughout this work, we have strived to make the REPL of the new system provide a user experience as close to HOL Light's as possible. To this end, we have, e.g., made the new system parse the same variant of OCaml syntax as HOL Light. All of the work described in this paper has been carried out in the HOL4 theorem prover.
|
|
| 5. |
- Abrahamsson, Oskar, 1986, et al.
(författare)
-
Fast, Verified Computation for Candle
- 2023
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. ; 268
-
Konferensbidrag (refereegranskat)abstract
- This paper describes how we have added an efficient function for computation to the kernel of the Candle interactive theorem prover. Candle is a CakeML port of HOL Light which we have, in prior work, proved sound w.r.t. the inference rules of the higher-order logic. This paper extends the original implementation and soundness proof with a new kernel function for fast computation. Experiments show that the new computation function is able to speed up certain evaluation proofs by several orders of magnitude.
|
|
| 6. |
- Abrahamsson, Oskar, 1986, et al.
(författare)
-
Proof-Producing Synthesis of CakeML from Monadic HOL Functions
- 2020
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 64:7, s. 1287-1306
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the instruction encoder and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem prover.
|
|
| 7. |
- Abrahamsson, Oskar, 1986
(författare)
-
Verified proof checking for higher-order logic
- 2020
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)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. To the best of our knowledge, this is the only proof checker for HOL that has been verified to this degree of rigor. Mathematical proofs exist to provide a high degree of confidence in the truth of statements. The level of confidence we place in a proof depends on its correctness. This correctness is usually established through proof checking, performed either by human or machine. One benefit of using a machine for this task is that the correctness of the machine itself can be proven. The main contribution of this work is a verified mechanized proof checker for theorems in higher-order logic (HOL). The checker is implemented as functions in the logic of the HOL4 theorem prover, and it comes with a soundness result, which states that it will only accept proofs of true theorems of HOL. Using a technique for proof-producing code generation (which is extended as part of this thesis), we synthesize a CakeML program that is compiled using the CakeML compiler. The CakeML compiler is verified to preserve program semantics. As a consequence, we are able to obtain a soundness result about the machine code which implements the proof checker.
|
|
| 8. |
- Ho, Son, et al.
(författare)
-
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
- 2018
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 10900, s. 646-662
-
Konferensbidrag (refereegranskat)abstract
- We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the type inferencer and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem prover.
|
|
| 9. |
- Kanabar, Hrutvik, et al.
(författare)
-
PureCake: A Verified Compiler for a Lazy Functional Language
- 2023
-
Ingår i: Proceedings of the ACM on Programming Languages. - 2475-1421. ; 7
-
Tidskriftsartikel (refereegranskat)abstract
- We present PureCake, a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. We derive sound equational reasoning principles over its operational semantics, dramatically simplifying some proofs. We prove end-To-end correctness for the compilation of PureLang down to machine code-The first such result for any lazy language-by targeting CakeML and composing with its verified compiler. Multiple optimisation passes are necessary to handle realistic lazy idioms effectively. We develop PureCake entirely within the HOL4 interactive theorem prover.
|
|
| 10. |
- Kotze, Shelley, 1986, et al.
(författare)
-
Walking as a pedagogical tool in higher education: Moving beyond COVID-19
- 2022
-
Ingår i: Royal Geographical Society (with IBG) Annual International Conference 2022.
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- In the wake of the COVID-19 pandemic, many pedagogical lessons have been drawn within higher education. However, the focus remains around digitalisation and distance education. Conversely, walking has been encouraged in everyday life throughout the pandemic, as a means of socialising, increasing health and wellbeing, and within professional environments. Whilst the use of walking as pedagogy method has been promoted within the education of younger children, its use in higher education has yet to be fully explored. Drawing upon our own experiences of teaching and being taught during the COVID-19 pandemic, and walking methodologies, this conceptual paper will discuss the potential of walking in higher education. We start from the position that walking, as a form of movement, is beneficial to learning, and outlines some of the multifaceted motivations we, as teachers (and students), have for introducing walking as pedagogy within higher education. Within this conceptual paper we explore the conceptualisation of both ‘thinking and walking’ and ‘walking and thinking’, as beneficial to academic learning and wellness respectively. Furthermore, we question whether the geographical context in which walking takes place has an influence on thinking and learning whilst walking. Finally, we offer some suggestions as to how walking pedagogies may be included in post-COVID pedagogies in higher education.
|
|
