Open Access. Powered by Scholars. Published by Universities.®
Programming Languages and Compilers Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Discipline
Articles 1 - 2 of 2
Full-Text Articles in Programming Languages and Compilers
The Algebra Of Type Unification, Verity James Scheel
The Algebra Of Type Unification, Verity James Scheel
Senior Projects Spring 2022
Type unification takes type inference a step further by allowing non-local flow of information. By exposing the algebraic structure of type unification, we obtain even more flexibility as well as clarity in the implementation. In particular, the main contribution is an explicit description of the arithmetic of universe levels and consistency of constraints of universe levels, with hints at how row types and general unification/subsumption can fit into the same framework of constraints. The compositional nature of the algebras involved ensure correctness and reduce arbitrariness: properties such as associativity mean that implementation details of type inference do not leak in …
Relating Justification Logic Modality And Type Theory In Curry–Howard Fashion, Konstantinos Pouliasis
Relating Justification Logic Modality And Type Theory In Curry–Howard Fashion, Konstantinos Pouliasis
Dissertations, Theses, and Capstone Projects
This dissertation is a work in the intersection of Justification Logic and Curry--Howard Isomorphism. Justification logic is an umbrella of modal logics of knowledge with explicit evidence. Justification logics have been used to tackle traditional problems in proof theory (in relation to Godel's provability) and philosophy (Gettier examples, Russel's barn paradox). The Curry--Howard Isomorphism or proofs-as-programs is an understanding of logic that places logical studies in conjunction with type theory and -- in current developments -- category theory. The point being that understanding a system as a logic, a typed calculus and, a language of a class of categories constitutes …