# Tag Info

Accepted

### What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator?

The definition is straightforward and can be found e.g. in (1, 2), see also (3). Here is a short summary, using a typed $\lambda$-calculus as basis. Types are not really needed for the presentation of ...
• 10.3k

### Proof that the calculus of constructions extended with recursive types isn't strongly normalizing?

With general recursive types you can define the type type T = T -> T With that type you can type self-application -- and in fact, every term of the untyped ...
• 1,290
Accepted

### Strong normalization property of CoC inside CoC

I'll summarize the comments from chi, and sketch the proof that There can be no proof of $\mathrm{False}:=\forall X:*.X$ in the CoC in head normal form. Furthermore, this fact can be proven in a weak ...
• 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
Accepted

• 13.2k

### Converting Kuroda normal form rules to the Penttonen normal form

You can find the proof in Penttonen's original research article: Martti Penttonen, One-Sided and Two-Sided Context in Formal Grammars. Information and Control 25, pp. 371-392 (1974). https://doi.org/...
• 5,424
Accepted

### References on implementing universe levels over MLTT?

IMHO universe hierarchy is particularly complicated to implement while the benefit is very small. It complicates programming in the language and the implementation of the language. The only benefit is ...
• 923
1 vote

### What technique is used to implement type checking for CoC?

I have a shorter answer: normalization is usually used in conversion check of terms (aka definitional equality), and CoC has untyped conversion check. In conversion check, we normalize terms and ...
• 923

Only top scored, non community-wiki answers of a minimum length are eligible