NB
Nathaniel Burke
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
6 records found
1
Dependently typed languages and proof assistants such as Agda and Rocq improve the reliability of mathematical proofs and programs by representing logical propositions as types and proofs as programs inhabiting those types. Through the Curry--Howard correspondence, typechecking becomes proof checking, allowing correctness guarantees to be established by construction.
However, these guarantees ultimately rely on the correctness of the language implementation itself. Components such as typecheckers, conversion checkers, and termination checkers are typically implemented as algorithms whose correctness must be trusted independently from the theory they are intended to enforce.
Agda Core is a core language for Agda implemented in Agda itself, where language judgements are represented directly as dependent types and checking procedures become programs constructing evidence of those judgements. This thesis investigates how the same methodology can be applied to termination checking.
Termination checking is a fundamental component of dependently typed languages, since unrestricted recursion may compromise normalization and logical consistency. We explore how termination criteria can be represented as formal specifications together with executable proof-search procedures producing explicit certificates that the criteria hold.
We first study the guard condition, a structural recursion criterion based on descending recursive arguments, and implement a certified checker producing explicit evidence that the criterion holds. We then investigate the size change principle, a stronger termination criterion capable of handling a wider class of recursive and mutually recursive definitions. We formalize the corresponding rules in the same framework and discuss the challenges involved in constructing a fully executable checker for them.
More generally, this work explores the separation between declarative specifications of termination criteria and the algorithms used to search for certificates satisfying them. By expressing termination arguments directly in the type theory of the implementation language, the resulting infrastructure becomes simultaneously executable, inspectable, and partially verified.
...
However, these guarantees ultimately rely on the correctness of the language implementation itself. Components such as typecheckers, conversion checkers, and termination checkers are typically implemented as algorithms whose correctness must be trusted independently from the theory they are intended to enforce.
Agda Core is a core language for Agda implemented in Agda itself, where language judgements are represented directly as dependent types and checking procedures become programs constructing evidence of those judgements. This thesis investigates how the same methodology can be applied to termination checking.
Termination checking is a fundamental component of dependently typed languages, since unrestricted recursion may compromise normalization and logical consistency. We explore how termination criteria can be represented as formal specifications together with executable proof-search procedures producing explicit certificates that the criteria hold.
We first study the guard condition, a structural recursion criterion based on descending recursive arguments, and implement a certified checker producing explicit evidence that the criterion holds. We then investigate the size change principle, a stronger termination criterion capable of handling a wider class of recursive and mutually recursive definitions. We formalize the corresponding rules in the same framework and discuss the challenges involved in constructing a fully executable checker for them.
More generally, this work explores the separation between declarative specifications of termination criteria and the algorithms used to search for certificates satisfying them. By expressing termination arguments directly in the type theory of the implementation language, the resulting infrastructure becomes simultaneously executable, inspectable, and partially verified.
...
Dependently typed languages and proof assistants such as Agda and Rocq improve the reliability of mathematical proofs and programs by representing logical propositions as types and proofs as programs inhabiting those types. Through the Curry--Howard correspondence, typechecking becomes proof checking, allowing correctness guarantees to be established by construction.
However, these guarantees ultimately rely on the correctness of the language implementation itself. Components such as typecheckers, conversion checkers, and termination checkers are typically implemented as algorithms whose correctness must be trusted independently from the theory they are intended to enforce.
Agda Core is a core language for Agda implemented in Agda itself, where language judgements are represented directly as dependent types and checking procedures become programs constructing evidence of those judgements. This thesis investigates how the same methodology can be applied to termination checking.
Termination checking is a fundamental component of dependently typed languages, since unrestricted recursion may compromise normalization and logical consistency. We explore how termination criteria can be represented as formal specifications together with executable proof-search procedures producing explicit certificates that the criteria hold.
We first study the guard condition, a structural recursion criterion based on descending recursive arguments, and implement a certified checker producing explicit evidence that the criterion holds. We then investigate the size change principle, a stronger termination criterion capable of handling a wider class of recursive and mutually recursive definitions. We formalize the corresponding rules in the same framework and discuss the challenges involved in constructing a fully executable checker for them.
More generally, this work explores the separation between declarative specifications of termination criteria and the algorithms used to search for certificates satisfying them. By expressing termination arguments directly in the type theory of the implementation language, the resulting infrastructure becomes simultaneously executable, inspectable, and partially verified.
However, these guarantees ultimately rely on the correctness of the language implementation itself. Components such as typecheckers, conversion checkers, and termination checkers are typically implemented as algorithms whose correctness must be trusted independently from the theory they are intended to enforce.
Agda Core is a core language for Agda implemented in Agda itself, where language judgements are represented directly as dependent types and checking procedures become programs constructing evidence of those judgements. This thesis investigates how the same methodology can be applied to termination checking.
Termination checking is a fundamental component of dependently typed languages, since unrestricted recursion may compromise normalization and logical consistency. We explore how termination criteria can be represented as formal specifications together with executable proof-search procedures producing explicit certificates that the criteria hold.
We first study the guard condition, a structural recursion criterion based on descending recursive arguments, and implement a certified checker producing explicit evidence that the criterion holds. We then investigate the size change principle, a stronger termination criterion capable of handling a wider class of recursive and mutually recursive definitions. We formalize the corresponding rules in the same framework and discuss the challenges involved in constructing a fully executable checker for them.
More generally, this work explores the separation between declarative specifications of termination criteria and the algorithms used to search for certificates satisfying them. By expressing termination arguments directly in the type theory of the implementation language, the resulting infrastructure becomes simultaneously executable, inspectable, and partially verified.
Bridging the Gap in Software Verification - Agda Proofs to Haskell Test Case Generators
How can preconditions in Agda be translated to a QuickCheck generator in Haskell?
Property-based testing is a popular testing paradigm, especially common in the functional programming language Haskell through the QuickCheck library. On the other hand, Agda is a dependently-typed language used as a proof assistant and for software verification. Because of the need for software verification, Agda2hs was created as a tool for translating code between these two, combining proven functionality with practical execution.
This work explores making QuickCheck-compatible generators based on properties encoded in Agda. This should allow automating early checking of Agda proofs for correctness, as well as enabling conversion of formal specifications to executable tests for Haskell projects. A procedure is presented that permits creating advanced generators and checkers, and it is later evaluated in terms of multifaceted performance metrics. ...
This work explores making QuickCheck-compatible generators based on properties encoded in Agda. This should allow automating early checking of Agda proofs for correctness, as well as enabling conversion of formal specifications to executable tests for Haskell projects. A procedure is presented that permits creating advanced generators and checkers, and it is later evaluated in terms of multifaceted performance metrics. ...
Property-based testing is a popular testing paradigm, especially common in the functional programming language Haskell through the QuickCheck library. On the other hand, Agda is a dependently-typed language used as a proof assistant and for software verification. Because of the need for software verification, Agda2hs was created as a tool for translating code between these two, combining proven functionality with practical execution.
This work explores making QuickCheck-compatible generators based on properties encoded in Agda. This should allow automating early checking of Agda proofs for correctness, as well as enabling conversion of formal specifications to executable tests for Haskell projects. A procedure is presented that permits creating advanced generators and checkers, and it is later evaluated in terms of multifaceted performance metrics.
This work explores making QuickCheck-compatible generators based on properties encoded in Agda. This should allow automating early checking of Agda proofs for correctness, as well as enabling conversion of formal specifications to executable tests for Haskell projects. A procedure is presented that permits creating advanced generators and checkers, and it is later evaluated in terms of multifaceted performance metrics.
agda2hs is a compiler that allows compilation of dependently typed Agda language into readable Haskell modules. This has a benefit that a formal proof of correctness can be carried out on Agda side, and then used in more realistic context in Haskell. However, sometimes it might be beneficial to compile yet unproven functions to Haskell, to be able to use traditional testing methods to quickly discard incorrect implementations. In this paper, I explore the usefulness of using mutation testing in validating such property tests. I present modifications made to the existing Haskell MuCheck library to accommodate this workflow: a QuickCheck test adapter, an annotation mechanism that links tests to the functions they cover, and a way to mark already proven functions so they are not mutated. I evaluate the tool on several test cases, both written by hand and generated from Agda, including sorting algorithms and lambda calculus with De Bruijn indices. I find that the share of mutants equivalent to the original code varies greatly between functions, which makes the ratio of killed mutants hard to interpret on its own. The current implementation does not prove very practical at this stage, and I propose some improvements that could make this a useful tool for this particular workflow.
...
agda2hs is a compiler that allows compilation of dependently typed Agda language into readable Haskell modules. This has a benefit that a formal proof of correctness can be carried out on Agda side, and then used in more realistic context in Haskell. However, sometimes it might be beneficial to compile yet unproven functions to Haskell, to be able to use traditional testing methods to quickly discard incorrect implementations. In this paper, I explore the usefulness of using mutation testing in validating such property tests. I present modifications made to the existing Haskell MuCheck library to accommodate this workflow: a QuickCheck test adapter, an annotation mechanism that links tests to the functions they cover, and a way to mark already proven functions so they are not mutated. I evaluate the tool on several test cases, both written by hand and generated from Agda, including sorting algorithms and lambda calculus with De Bruijn indices. I find that the share of mutants equivalent to the original code varies greatly between functions, which makes the ratio of killed mutants hard to interpret on its own. The current implementation does not prove very practical at this stage, and I propose some improvements that could make this a useful tool for this particular workflow.
Proving with the Help of Property-Based Testing
Exposing the QuickCheck Interface in Agda for Agda2Hs
Testing constitutes an important part of software development for many engineers. Agda2Hs, a transpiler from Agda to Haskell, currently does not provide such testing functionality. Agda enables developers to express and formally verify properties directly within the source code, whereas Haskell benefits from an extensive ecosystem of tools and developers. By transpiling verified Agda code to Haskell, Agda2Hs offers the potential to combine the advantages of both languages. However, constructing formal proofs in Agda is challenging, as it requires the same creativity and insight needed for mathematical reasoning. Consequently, a proposition with a bug may be mistakenly seen as difficult to prove. Property-based testing can provide confidence in the correctness of a proposition before a proof is completed. This paper presents these testing functionalities in Agda2Hs by porting QuickCheck to Agda. Furthermore, correspondence proofs are introduced, which enable programmers to show formally that a test asserts the same property as a proposition.
...
Testing constitutes an important part of software development for many engineers. Agda2Hs, a transpiler from Agda to Haskell, currently does not provide such testing functionality. Agda enables developers to express and formally verify properties directly within the source code, whereas Haskell benefits from an extensive ecosystem of tools and developers. By transpiling verified Agda code to Haskell, Agda2Hs offers the potential to combine the advantages of both languages. However, constructing formal proofs in Agda is challenging, as it requires the same creativity and insight needed for mathematical reasoning. Consequently, a proposition with a bug may be mistakenly seen as difficult to prove. Property-based testing can provide confidence in the correctness of a proposition before a proof is completed. This paper presents these testing functionalities in Agda2Hs by porting QuickCheck to Agda. Furthermore, correspondence proofs are introduced, which enable programmers to show formally that a test asserts the same property as a proposition.
Specified Agda is Testable Haskell
Translating Agda Postconditions to QuickCheck Property Tests in agda2hs
Formally verified code written in dependently typed languages can be integrated into larger, non-verified code bases through source-to-source translation. The agda2hs compiler enables such integration by translating verified Agda code to readable Haskell, erasing proofs and type indices in the process. The properties that a program is verified against are encoded as such proofs and type indices, and are therefore also erased. Yet being able to check these properties is important: in the agda2hs workflow, verified code may depend on unverified Haskell libraries whose properties are assumed without proof and never tested.
In this paper, we present an extension to agda2hs that extracts postconditions and translates them into Haskell QuickCheck property tests. Since postconditions in Agda are encoded at the type level, they are not executable and cannot be translated to Haskell directly. We address this by deriving semi-decision procedures that check whether a proposition holds for given inputs. We cover postconditions expressed as separate lemmas, sigma types, and indexed datatypes. We implement lemma-to-test translation as a working agda2hs extension; it requires the user to write the decision procedure by hand. We present the automatic derivation of such procedures as an algorithm design with worked examples. ...
In this paper, we present an extension to agda2hs that extracts postconditions and translates them into Haskell QuickCheck property tests. Since postconditions in Agda are encoded at the type level, they are not executable and cannot be translated to Haskell directly. We address this by deriving semi-decision procedures that check whether a proposition holds for given inputs. We cover postconditions expressed as separate lemmas, sigma types, and indexed datatypes. We implement lemma-to-test translation as a working agda2hs extension; it requires the user to write the decision procedure by hand. We present the automatic derivation of such procedures as an algorithm design with worked examples. ...
Formally verified code written in dependently typed languages can be integrated into larger, non-verified code bases through source-to-source translation. The agda2hs compiler enables such integration by translating verified Agda code to readable Haskell, erasing proofs and type indices in the process. The properties that a program is verified against are encoded as such proofs and type indices, and are therefore also erased. Yet being able to check these properties is important: in the agda2hs workflow, verified code may depend on unverified Haskell libraries whose properties are assumed without proof and never tested.
In this paper, we present an extension to agda2hs that extracts postconditions and translates them into Haskell QuickCheck property tests. Since postconditions in Agda are encoded at the type level, they are not executable and cannot be translated to Haskell directly. We address this by deriving semi-decision procedures that check whether a proposition holds for given inputs. We cover postconditions expressed as separate lemmas, sigma types, and indexed datatypes. We implement lemma-to-test translation as a working agda2hs extension; it requires the user to write the decision procedure by hand. We present the automatic derivation of such procedures as an algorithm design with worked examples.
In this paper, we present an extension to agda2hs that extracts postconditions and translates them into Haskell QuickCheck property tests. Since postconditions in Agda are encoded at the type level, they are not executable and cannot be translated to Haskell directly. We address this by deriving semi-decision procedures that check whether a proposition holds for given inputs. We cover postconditions expressed as separate lemmas, sigma types, and indexed datatypes. We implement lemma-to-test translation as a working agda2hs extension; it requires the user to write the decision procedure by hand. We present the automatic derivation of such procedures as an algorithm design with worked examples.
This research aims to explore using property based testing to find counterexamples for proving statements about programs in Agda2hs. I have created an extension to Agda2hs to translate type class laws into QuickCheck properties and evaluated on real-world Haskell code to evaluate its effectiveness. I found that having relatively cheap to run tests compared to formalizing helped save time ensuring definitions were correct before formalizing statements.
...
This research aims to explore using property based testing to find counterexamples for proving statements about programs in Agda2hs. I have created an extension to Agda2hs to translate type class laws into QuickCheck properties and evaluated on real-world Haskell code to evaluate its effectiveness. I found that having relatively cheap to run tests compared to formalizing helped save time ensuring definitions were correct before formalizing statements.