LE
L.F.B. Escot
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>
5 records found
1
Dependently-typed languages allow one to guarantee correctness of a program by providing formal proofs. The type checkers of such languages elaborate the user-friendly high-level surface language to a small and fully explicit core language. A lot of trust is put into this elaboration process, even though it is rarely verified. One such elaboration is elaborating dependent pattern matching to the low-level construction of eliminators. This elaboration is done in two steps. First, the function defined by dependent pattern matching is translated into a case tree, which can then be further translated to eliminators. We present a generic, well-typed implementation of this second step in Agda, without the use of metaprogramming and unsafe transformations, by providing a type-safe, correct-by construction, generic definition of case trees and an evaluation function that, given an interpretation of such a case tree and an interpretation of the telescope of function arguments, evaluates the output term of the function using only eliminators. We only allow case splits on variables from a fixed universe of data type descriptions, for which we use techniques like basic analysis and specialization by unification.
...
...
Dependently-typed languages allow one to guarantee correctness of a program by providing formal proofs. The type checkers of such languages elaborate the user-friendly high-level surface language to a small and fully explicit core language. A lot of trust is put into this elaboration process, even though it is rarely verified. One such elaboration is elaborating dependent pattern matching to the low-level construction of eliminators. This elaboration is done in two steps. First, the function defined by dependent pattern matching is translated into a case tree, which can then be further translated to eliminators. We present a generic, well-typed implementation of this second step in Agda, without the use of metaprogramming and unsafe transformations, by providing a type-safe, correct-by construction, generic definition of case trees and an evaluation function that, given an interpretation of such a case tree and an interpretation of the telescope of function arguments, evaluates the output term of the function using only eliminators. We only allow case splits on variables from a fixed universe of data type descriptions, for which we use techniques like basic analysis and specialization by unification.
A Computer-Checked Library of Category Theory
Functors and F-Coalgebras
This research project aims to develop a computer-checked library of category theory within the Lean proof assistant, with a specific emphasis on concepts and examples relevant to functional programming. Category theory offers a robust mathematical framework that allows for the abstraction and comprehension of concepts across diverse fields, including computer science. Additionally, the project will explore the application of final coalgebras, particularly in the context of understanding infinite data structures. By creating a formalized category theory library within Lean, our objective is to enhance our understanding of functional programming and programming language concepts. Moreover, we aim to facilitate the study of these topics by providing a comprehensible library and a rigorous foundation for program reasoning, thereby benefiting researchers and practitioners in the field.
...
This research project aims to develop a computer-checked library of category theory within the Lean proof assistant, with a specific emphasis on concepts and examples relevant to functional programming. Category theory offers a robust mathematical framework that allows for the abstraction and comprehension of concepts across diverse fields, including computer science. Additionally, the project will explore the application of final coalgebras, particularly in the context of understanding infinite data structures. By creating a formalized category theory library within Lean, our objective is to enhance our understanding of functional programming and programming language concepts. Moreover, we aim to facilitate the study of these topics by providing a comprehensible library and a rigorous foundation for program reasoning, thereby benefiting researchers and practitioners in the field.
Dependent programming languages such as Agda show a lot of promise in creating new ways of writing code, but currently suffer from a lack of support and features. In this paper we attempt to create a new back-end for Agda targeting Java which has a huge and thriving ecosystem.
We implement the new back-end for Agda in Haskell and we describe the benefits and drawbacks of targeting Java. Firstly we go into the existing methods of compiler Agda, then we go into how to compile Agda to Java and what the main challenges where creating the compiler and what solutions were implemented to solve these. Afterwards Agda2Java is compared to the existing methods of compiling Agda code by means of benchmarks and analyzing the execution time. We show that at its current state, Java does not seem to be a promising back-end for Agda, but that there is work being done on Java that might change this perception. ...
We implement the new back-end for Agda in Haskell and we describe the benefits and drawbacks of targeting Java. Firstly we go into the existing methods of compiler Agda, then we go into how to compile Agda to Java and what the main challenges where creating the compiler and what solutions were implemented to solve these. Afterwards Agda2Java is compared to the existing methods of compiling Agda code by means of benchmarks and analyzing the execution time. We show that at its current state, Java does not seem to be a promising back-end for Agda, but that there is work being done on Java that might change this perception. ...
Dependent programming languages such as Agda show a lot of promise in creating new ways of writing code, but currently suffer from a lack of support and features. In this paper we attempt to create a new back-end for Agda targeting Java which has a huge and thriving ecosystem.
We implement the new back-end for Agda in Haskell and we describe the benefits and drawbacks of targeting Java. Firstly we go into the existing methods of compiler Agda, then we go into how to compile Agda to Java and what the main challenges where creating the compiler and what solutions were implemented to solve these. Afterwards Agda2Java is compared to the existing methods of compiling Agda code by means of benchmarks and analyzing the execution time. We show that at its current state, Java does not seem to be a promising back-end for Agda, but that there is work being done on Java that might change this perception.
We implement the new back-end for Agda in Haskell and we describe the benefits and drawbacks of targeting Java. Firstly we go into the existing methods of compiler Agda, then we go into how to compile Agda to Java and what the main challenges where creating the compiler and what solutions were implemented to solve these. Afterwards Agda2Java is compared to the existing methods of compiling Agda code by means of benchmarks and analyzing the execution time. We show that at its current state, Java does not seem to be a promising back-end for Agda, but that there is work being done on Java that might change this perception.
Formal verification works better than testing, since the correctness of a program is proven. It is researched if it is possible and feasible to formally verify the Inductive Graph Library. The library is an abstract class in Haskell and is ported manually to Agda. Agda is a total and dependently typed language and thus can be used as a proof assistant. The functions are first converted to total functions and the preconditions the are proven. Verifying an abstract class is time consuming, since it requires an implemented instance of the abstract class. Stating the properties of the library is possible, but difficult since it requires generalised properties that need to be valid for all instances of the abstract class. The verification process is not completed yet, so no definitive conclusions are made, but the properties that are verified did not produce any issues. agda2hs is used to compile the Agda code to Haskell, this ensures that the verified Agda code is verified Haskell code. This requires the library to fall within the common subset of agda2hs.
...
Formal verification works better than testing, since the correctness of a program is proven. It is researched if it is possible and feasible to formally verify the Inductive Graph Library. The library is an abstract class in Haskell and is ported manually to Agda. Agda is a total and dependently typed language and thus can be used as a proof assistant. The functions are first converted to total functions and the preconditions the are proven. Verifying an abstract class is time consuming, since it requires an implemented instance of the abstract class. Stating the properties of the library is possible, but difficult since it requires generalised properties that need to be valid for all instances of the abstract class. The verification process is not completed yet, so no definitive conclusions are made, but the properties that are verified did not produce any issues. agda2hs is used to compile the Agda code to Haskell, this ensures that the verified Agda code is verified Haskell code. This requires the library to fall within the common subset of agda2hs.
Agda2hs is a program which compiles a subset of Agda to Haskell. In this paper, an implementation of the Haskell library QuadTree is created and verified in this subset of Agda, such that Agda2hs can then produce a verified Haskell implementation. To aid with this verification, a number of techniques have been proposed which are used to prove invariants, preconditions and post-conditions of the QuadTree library. Using these techniques, the properties of the library have been proven. Additionally, recommendations are made to reduce the time needed for verification.
...
Agda2hs is a program which compiles a subset of Agda to Haskell. In this paper, an implementation of the Haskell library QuadTree is created and verified in this subset of Agda, such that Agda2hs can then produce a verified Haskell implementation. To aid with this verification, a number of techniques have been proposed which are used to prove invariants, preconditions and post-conditions of the QuadTree library. Using these techniques, the properties of the library have been proven. Additionally, recommendations are made to reduce the time needed for verification.