New answers tagged

1 vote

Adding type constructors to universes

$Γ.\mathrm{El}(a) ⊢ U\ \mathrm{type}$ is valid because $Γ ⊢ U\ \mathrm{type}$ is valid for all $Γ$. Just pick $Γ.\mathrm{El}(a)$ as the context. For one, there is no reason to have the $a$ in that ...
Dan Doel's user avatar
  • 2,687
2 votes

Relation between Curry-Howard isomorphism and Kripke semantics for intuitionistic logic

For propositional logic, you're probably right. As far as quantifier logic goes: the Curry-Howard correspondence never included quantifiers and there isn't really any consensus or standard treatment ...
NinjaDarth's user avatar
0 votes

Reference types

In Swift, there is a conscious distinction between "reference types" and "value types". classes and closures are reference types, structs, enums, and tuples are value types. If you ...
gnasher729's user avatar
0 votes

Characterization of lambda-terms that have union types

The standard approach is to expand the Curry-Howard Correspondence to cover disjunctions by providing cover for the tautologies: $$ O: (a ⊃ c) ⊃ (b ⊃ c) ⊃ a ∨ b ⊃ c,\quad 𝐝: a ⊃ a ∨ b,\quad 𝐪: b ⊃ a ...
NinjaDarth's user avatar
0 votes

Does the Y combinator contradict the Curry-Howard correspondence?

Look at the construction for $Y = λf·(λx·f (x x))(λx·f (x x))$. Carefully apply the type rules to it $$\begin{align} f:& C → A,\\ x:& B → C,\\ x:& B,\\ x x:& C,\\ f (x x):& A,\\ λx·...
NinjaDarth's user avatar

Top 50 recent answers are included