New answers tagged type-theory
1
You can: define /hereditary substitution/ on already normalized STLC terms using structural induction (where the induction is (in part) on the type).
I couldn't find the reference I was thinking of right now, but a quick search for "agda hereditary subtitutions STLC" pointed to various relevant pages, such as https://github.com/ezyang/lr-agda/blob/...
3
Take any small symmetric monoidal category $V$.
Then the category of $V$-valued presheaves will (a) have closed monoidal structure (via Day convolution), and (b) have enough stuff (inherited from $\mathrm{Set}$) to interpret dependent types. This gives you enough structure to interpret something like our LNL calculus pretty easily, because there is a nice ...
Top 50 recent answers are included
Related Tags
type-theory × 306lo.logic × 84
pl.programming-languages × 73
lambda-calculus × 66
dependent-type × 66
type-systems × 42
type-inference × 32
reference-request × 27
ct.category-theory × 21
calculus-of-constructions × 21
functional-programming × 20
coq × 20
typed-lambda-calculus × 18
proof-theory × 15
homotopy-type-theory × 12
proof-assistants × 11
polymorphism × 10
computability × 9
automated-theorem-proving × 9
linear-logic × 6
constructive-mathematics × 6
curry-howard × 6
soft-question × 5
set-theory × 5
haskell × 5