# Tag Info

Accepted

### How do you get the Calculus of Constructions from the other points in the Lambda Cube?

First, to reiterate one of cody's points, the Calculus of Inductive Constructions (which Coq's kernel is based on) is very different from the Calculus of Constructions. It is best thought of as ...
• 31.6k

### How do you get the Calculus of Constructions from the other points in the Lambda Cube?

I've often wanted to try and summarize each dimension of the $\lambda$-cube and what they represent, so I'll give this one a shot. But first, one should probably try to dis-entangle various issues. ...
• 13.2k

### Is there a typed lambda calculus which is consistent and Turing complete?

Alright I'll give a crack at it: In general for a given type system $T$, the following is true: If all well-type terms in the calculus $T$ are normalizing, then $T$ is consistent when viewed as a ...
• 13.2k
Accepted

• 4,823
Accepted

### Proof techniques for showing that dependent type checking is decidable

There is indeed a subtlety here, though things work out nicely in the case of type checking. I'll write down the issue here, since it seems to come up in many related threads, and try to explain why ...
• 13.2k
Accepted

### Recursive types and the empty type

First, note that nothing turns on the presence or absence of the empty type: if you have a nonlinear calculus with function types and unrestricted recursive types, then it is inconsistent. Indeed, ...
• 31.6k

### Can typed lambda calculi express *all* algorithms below a given complexity?

I'll try to complement Damiano's excellent answer. In general a typed $\lambda$-calculus can be used as a language of realizers for a certain logic. In particular system $F$ is a language of ...
• 13.2k
Accepted

### Calculus of Constructions: compress expression to its smallest form

There's a bit of freedom in what we considre "the same value". Let me show that there is no such algorithm if "the same value" means "observationally equivalent". I will use a fragment of the Calculus ...
• 26.6k

### Calculus of Constructions: compress expression to its smallest form

As Andrej has said, the problem is undecidable if you allow replacing one term by another, extensionally equal one. However, you might be interested in optimal sharing of expressions, in the following ...
• 13.2k

### Eta expansion in the pattern lambda calculus

This is not a complete answer; it is a comment that got too large. If you extend typed lambda calculus with products with projective eliminators (ie, product eliminators ...
• 31.6k

### Typing of substitution in a bidirectional type system

One solution is indeed to restrict to substituting with synthesizing expressions. You can only hope to replace variables with terms of the same mode (i.e. inferrable terms), anything else just won't ...
• 636
Accepted

### Typing of substitution in a bidirectional type system

The key observation is that whether the substitution theorem holds, depends on the definition of substitution. For the usual definition of substitution of terms for variables, the substitution ...
• 31.6k
Accepted

### Understanding the Proof of Strong Normalization of the Calculus of Constructions

Unfortunately, I'm not sure there are more beginner friendly resources than Geuvers' account. You might try this note from Chris Casinghino which gives an account of several proofs in excruciating ...
• 13.2k
Accepted

### Structural equality of Pi Types with heterogeneous equality?

I am not aware that J or K exists for heterogeneous equality. It does not need an elimination principle, because it can be simply defined as a sigma type: ...
• 1,349