The systems of the λ-cube have the axiom $\star:\square$. I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below. What are the intuitive meanings of $\star$ and ...
Mathematically, I know what a semigroup is: It is a set S along with an associative binary operation $* : S \times S \rightarrow S$. So far, so good. From a computational perspective, one can ...
I am interested in learning the theory of types, especially in how they can provide a foundation to mathematics different to sets and how they can avoid self-referential paradoxes by stipulating that ...
I am aware that assigning the type of Type to be Type (rather than stratifying to a hierarchy of types) leads to an inconsistency. But does this inconsistency allow the construction of a well-typed ...
Please forgive any unorthodox notation or obvious errors here... I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the ...
Palmgren (1997), On universes in type theory, discusses work of several theorists that provide what we might call a family of Large Universe Axioms (LUAs) for predicative type theory, culminating in ...
Is there such a thing as "recursively dependent types"? Specifically, I would like a dependent type theory containing a type $A(x)$ which depends on a variable $x: A(z)$, where $z$ is a particular ...
So I'm not much of a math guy but I've really enjoyed programming in Lisp and have become interested in the ideas of lambda calculus which it is based. I was wondering if anyone had a suggestion ...