Open Access. Powered by Scholars. Published by Universities.®
- Discipline
- Institution
- Publication Type
Articles 1 - 2 of 2
Full-Text Articles in Engineering
Approximation Of Nested Fixpoints, Alexander Kurz
Approximation Of Nested Fixpoints, Alexander Kurz
Engineering Faculty Articles and Research
The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible nontermination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekic lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is …
Irrelevance, Polymorphism, And Erasure In Type Theory, Richard Nathan Mishra-Linger
Irrelevance, Polymorphism, And Erasure In Type Theory, Richard Nathan Mishra-Linger
Dissertations and Theses
Dependent type theory is a proven technology for verified functional programming in which programs and their correctness proofs may be developed using the same rules in a single formal system. In practice, large portions of programs developed in this way have no computational relevance to the ultimate result of the program and should therefore be removed prior to program execution. In previous work on identifying and removing irrelevant portions of programs, computational irrelevance is usually treated as an intrinsic property of program expressions. We find that such an approach forces programmers to maintain two copies of commonly used datatypes: a …