Questions tagged [typed-lambda-calculus]

The tag has no usage guidance.

13 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
156 views

Constructive Strong Normalization of the Extended Calculus of Constructions

The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof ...
300 views

Denotational semantics of System $F_\omega$ with recursive types and general recursion

Is there a denotational semantics for System $F_\omega$ in literature that supports both recursive types and general recursion? I'm looking for a model of Ralf Hinze's variant of System $F_\omega$ [4]...
161 views

$\lambda$-definability and structure preserved by homomorphisms

I imagine there are some standard results that bear on this, but I'm having trouble finding a proof or refutation of it. Some prelimary definitions. A Henkin structure $A = (A^\cdot, ⟦\cdot⟧_A)$ for ...
150 views

Category theory lambda cube?

If simply typed lambda calculus corresponds to cartesian closed categories, what types of categories do other calculi in the lambda cube correspond to? https://en.m.wikipedia.org/wiki/Lambda_cube
87 views

Characterisation of the BCIW definable functions

Given a full model of the simply typed lambda calculus, it's possible to characterise the lambda definable functions as those that are invariant under every "Kripke logical relation". (See here.) I ...
86 views

Coherence spaces and full completeness for the implicative fragment of linear logic

Linear logic isn't complete for coherence space semantics since $1$ and $\top$ get identified. But it is, I believe, complete for the fragment of linear logic whose only connective is $\multimap$. I ...
112 views

Type System Of $\lambda\mu$-Calculus

reading this paper on CPS-tranformation from the $\lambda\mu$-calculus, I'm a bit confused about the type system presented: Why second-order formulas in the types? Is this according to the Curry-...
253 views

Is System-F with higher-kinded newtypes equivalent in computational power to System-F omega?

If we have System-F with higher-kinded types and newtypes, then we can express everything (I think) of System-F omega, except we have to manually (un)pack. For example: ...
53 views