Open Access. Powered by Scholars. Published by Universities.®
- Keyword
Articles 1 - 2 of 2
Full-Text Articles in Logic and Foundations
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 …
Constructing A Categorical Framework Of Metamathematical Comparison Between Deductive Systems Of Logic, Alex Gabriel Goodlad
Constructing A Categorical Framework Of Metamathematical Comparison Between Deductive Systems Of Logic, Alex Gabriel Goodlad
Senior Projects Spring 2016
The topic of this paper in a broad phrase is “proof theory". It tries to theorize the general
notion of “proving" something using rigorous definitions, inspired by previous less general
theories. The purpose for being this general is to eventually establish a rigorous framework
that can bridge the gap when interrelating different logical systems, particularly ones
that have not been as well defined rigorously, such as sequent calculus. Even as far as
semantics go on more formally defined logic such as classic propositional logic, concepts
like “completeness" and “soundness" between the “semantic" and the “deductive system"
is too arbitrarily defined …