Ad
A. de Vries
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>
2 records found
1
Software correctness is a hard problem. Dependently-typed programming languages like Agda help us to provide guarantees about software while writing it in a Correct-by-Construction (CbC) manner. However, the implementation of a dependently-typed programming language may contain bugs itself: Agda has bugs in its own implementation on a regular basis. Dependently typed-typed programming languages should therefore verify themselves in a Correct-by-Construction manner using their own components: self-verification. Agda Core aims to do this for Agda: it is a core language for Agda and provides a Correct-by-Construction type checker for itself derived from a trusted type theory, written in Agda.
Before Agda Core can be used as a true self-verifier for Agda and be integrated into Agda’s main compiler and type checker, more features from Agda need to be supported by it. In this thesis, we focus on Agda’s η-conversion for function types and record types. We formalize η-conversion for function types and record types with at least one field using untyped conversion: we also add support for records to Agda Core along the way. We also show progress towards a formalization of Agda’s η-conversion using typed conversion, which allows for formalizing the often tricky-considered η-conversion for Agda’s unit type. For all of these formalizations, we show that they can be added to Agda Core with reasonable effort. Overall, this work therefore provides an important step towards the ultimate goal of a self-verified type checker for Agda with support for all of Agda’s features, which decreases the future potential for bugs in Agda’s implementation with relation to η-conversion, and teaches us how to self-verify η-conversion for a dependently-typed language. ...
Before Agda Core can be used as a true self-verifier for Agda and be integrated into Agda’s main compiler and type checker, more features from Agda need to be supported by it. In this thesis, we focus on Agda’s η-conversion for function types and record types. We formalize η-conversion for function types and record types with at least one field using untyped conversion: we also add support for records to Agda Core along the way. We also show progress towards a formalization of Agda’s η-conversion using typed conversion, which allows for formalizing the often tricky-considered η-conversion for Agda’s unit type. For all of these formalizations, we show that they can be added to Agda Core with reasonable effort. Overall, this work therefore provides an important step towards the ultimate goal of a self-verified type checker for Agda with support for all of Agda’s features, which decreases the future potential for bugs in Agda’s implementation with relation to η-conversion, and teaches us how to self-verify η-conversion for a dependently-typed language. ...
Software correctness is a hard problem. Dependently-typed programming languages like Agda help us to provide guarantees about software while writing it in a Correct-by-Construction (CbC) manner. However, the implementation of a dependently-typed programming language may contain bugs itself: Agda has bugs in its own implementation on a regular basis. Dependently typed-typed programming languages should therefore verify themselves in a Correct-by-Construction manner using their own components: self-verification. Agda Core aims to do this for Agda: it is a core language for Agda and provides a Correct-by-Construction type checker for itself derived from a trusted type theory, written in Agda.
Before Agda Core can be used as a true self-verifier for Agda and be integrated into Agda’s main compiler and type checker, more features from Agda need to be supported by it. In this thesis, we focus on Agda’s η-conversion for function types and record types. We formalize η-conversion for function types and record types with at least one field using untyped conversion: we also add support for records to Agda Core along the way. We also show progress towards a formalization of Agda’s η-conversion using typed conversion, which allows for formalizing the often tricky-considered η-conversion for Agda’s unit type. For all of these formalizations, we show that they can be added to Agda Core with reasonable effort. Overall, this work therefore provides an important step towards the ultimate goal of a self-verified type checker for Agda with support for all of Agda’s features, which decreases the future potential for bugs in Agda’s implementation with relation to η-conversion, and teaches us how to self-verify η-conversion for a dependently-typed language.
Before Agda Core can be used as a true self-verifier for Agda and be integrated into Agda’s main compiler and type checker, more features from Agda need to be supported by it. In this thesis, we focus on Agda’s η-conversion for function types and record types. We formalize η-conversion for function types and record types with at least one field using untyped conversion: we also add support for records to Agda Core along the way. We also show progress towards a formalization of Agda’s η-conversion using typed conversion, which allows for formalizing the often tricky-considered η-conversion for Agda’s unit type. For all of these formalizations, we show that they can be added to Agda Core with reasonable effort. Overall, this work therefore provides an important step towards the ultimate goal of a self-verified type checker for Agda with support for all of Agda’s features, which decreases the future potential for bugs in Agda’s implementation with relation to η-conversion, and teaches us how to self-verify η-conversion for a dependently-typed language.
Non-Euclidean spaces are spaces that do not satisfy all of Euclid’s postulates. An example of such a space is hyperbolic space. In this paper, a method is discussed to draw a tessellation of hyperbolic space in a manner that fits with the virtual reality game "Holonomy", a game which takes place in hyperbolic space. The main result shows that the new approach is better in terms of simplicity than the old approach and is able to draw the game world more faithfully than the old approach. The features of the new approach could still be significantly expanded upon.
...
Non-Euclidean spaces are spaces that do not satisfy all of Euclid’s postulates. An example of such a space is hyperbolic space. In this paper, a method is discussed to draw a tessellation of hyperbolic space in a manner that fits with the virtual reality game "Holonomy", a game which takes place in hyperbolic space. The main result shows that the new approach is better in terms of simplicity than the old approach and is able to draw the game world more faithfully than the old approach. The features of the new approach could still be significantly expanded upon.