New answers tagged

8 votes

How exactly are realizability and the Curry-Howard correspondence related?

I am sure more than one exact correspondence can be made, but here's at least one that is technically precise. We shall employ categorical logic. Executive summary: realizability is the ...
Andrej Bauer's user avatar
  • 46.7k
2 votes

Does substitution on named terms correspond to substitution on de Bruijn terms?

See the 2021-present work of Joshua Grosso, who formalised the paper in Coq, correcting some errors in the process (last update 3 weeks ago). However, Grosso wrote: To our knowledge, all of the main ...
David Roberts's user avatar
  • 33.2k
1 vote

Constructing set-truncations of types from universes

Given a universe $U$, the type of $U$-small propositions is given by $$\mathrm{Prop} \equiv \sum_{P:U} \prod_{x:P} \prod_{y:P} x = y$$ Given a type $A:U$, for $x:A$ and $y:A$, the type $$[x = y] \...
Madeleine Birchfield's user avatar
1 vote

Why is there no product type in simply typed lambda-calculus?

In spite of all the interesting exchange that has gone back and forth about sum types, the original question about product types (‘how can one prove that the simply typed 𝜆-calculus does not support ...
provocateur's user avatar

Top 50 recent answers are included