Share Your Experience: Take the 2024 Developer Survey

# Questions tagged [calculus-of-constructions]

The tag has no usage guidance.

14 questions
Filter by
Sorted by
Tagged with
1 vote
23 views

### What is a simple explanation of how the calculus of inductive constructions is an extension of simply typed lambda calculus?

I’m doing some basic studying of lambda calculus and Coq and I’d like some supporting explanation about the relationship between lambda calculus and the calculus of inductive constructions. This ...
33 views

### Where can I find a list of logics with their corresponding calculus and computation phenomena?

I was watching some lectures by Prof. Pfenning on Proof Theory. Between 5:30 and 15:00, he gave a list for some different kinds of judgments along with their calculus and computation phenomena that ...
• 109
33 views

### What can we have in exchange if we drop subtyping from definition of Calculus of Inductive Constructions?

If we remove subtyping (https://coq.inria.fr/distrib/current/refman/language/cic.html#subtyping-rules) from CIC we will lose some expressive power. But is that power necessary for a programming ...
1 vote
66 views

### Lambda calculus and runtime inspection of the term

This is possibly related to reflection and quoting but I don't want to assume anything beforehand. Here is my requirement. My typed lambda calculus (Curry style) is a simpler variant of Calculus of ...
• 31
90 views

### Deriving recursive definition from function specification

Given this function specification, where name xs is bound to a list, # denotes its cardinality and ...
• 125
113 views

### Calculus of constructions, type-in-type and recursion

Does adding type-in-type to the calculus of constructions lead to (general) recursion? Such that one can write the Y combinator.
• 565
326 views

### What types are propositions?

In the propositions-as-types paradigm, we are still faced with the question : what types are propositions ? I currently know 3 different answers : Coq's sort Prop ...
• 153
101 views

### What untyped term inhabits induction on natural numbers in CoC?

Induction on Church-encoded natural numbers (which I will call indNat) can not be defined within the Calculus of Constructions. If we assumed ...
• 565
57 views

### Why 'let' can not be reduce to a lambda application in (extended) Calculus of Constructions

I do not understand the difference highlighted in the chapter 2.5 of the book Theorem Proving in Lean: Notice that the meaning of the expression let a := t1 in t2 is very similar to the meaning of (...
• 485