arXiv:1803.10143cs.LO
An extended type system with lambda-typed lambda-expressions
Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.
Abstract
We present the system $\mathtt{d}$, an extended type system with lambda-typed lambda-expressions. It is related to type systems originating from the Automath project. $\mathtt{d}$ extends existing lambda-typed systems by an existential abstraction operator as well as propositional operators. $β$-reduction is extended to also normalize negated expressions using a subset of the laws of classical negation, hence $\mathtt{d}$ is normalizing both proofs and formulas which are handled uniformly as functional expressions. $\mathtt{d}$ is using a reflexive type axiom for a constant $τ$ to which no function can be typed. Some properties are shown including confluence, subject reduction, uniqueness of types, strong normalization, and consistency. We illustrate how, when using $\mathtt{d}$, due to its limited logical strength, additional axioms must be added both for negation and for the mathematical structures whose deductions are to be formalized.
I think it’s referring to this definition from a 2018 paper: https://arxiv.org/abs/1803.10143 “An extended type system with lambda-typed lambda-expressions” If I understand it correctly, it implies that a type itself may be a function.
stingraycharlesView on HNParent context