Questions tagged [calculus-of-constructions]
The calculus-of-constructions tag has no usage guidance.
5
questions with no upvoted or accepted answers
3
votes
0
answers
112
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.
2
votes
0
answers
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
0
answers
22
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 ...
1
vote
0
answers
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 ...
0
votes
0
answers
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 ...