Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [calculus-of-constructions]

Filter by
Sorted by
Tagged with
1 vote
0 answers
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 ...
Julius Hamilton's user avatar
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 ...
geeko's user avatar
  • 109
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 ...
Maciej Poleski's user avatar
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 ...
Ram's user avatar
  • 31
2 votes
1 answer
90 views

Deriving recursive definition from function specification

Given this function specification, where name xs is bound to a list, # denotes its cardinality and ...
F. Zer's user avatar
  • 125
3 votes
0 answers
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.
Labbekak's user avatar
  • 565
5 votes
1 answer
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 ...
V. Semeria's user avatar
5 votes
1 answer
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 ...
Labbekak's user avatar
  • 565
5 votes
1 answer
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 (...
user3368561's user avatar
6 votes
1 answer
841 views

Where are C++ templates inside of the lambda cube?

C++ templates have type variables and can express lambdas, so they must have System F embedded. But is that exactly where they are located in the lambda cube? Can C++ templates produce new types or ...
Fomalhaut's user avatar
2 votes
1 answer
160 views

Understanding the definition of Positivity Constraints in Coq

In Interactive Theorem Proving and Program Development the authors explain constraints on constructors of inductive types in Coq. For inductive type $T$, a constructor must have the form $t_1 \...
Mark's user avatar
  • 215
2 votes
1 answer
431 views

Type Theory and Principia Mathematica Part IV "Relation Arithmetic"

As type theory is a principle focus of modern computer science, its origins are in Bertrand Russel's theory of types, Principia Mathematica is both the origin of and is expressed in the theory of ...
James Bowery's user avatar
11 votes
2 answers
1k views

Universal/existential quantification?

I'm struggling to understand the purpose of universal and existential quantification of types. I'm playing around with writing a toy language based on the calculus of constructions. I've been reading ...
oconnor0's user avatar
  • 393
6 votes
1 answer
230 views

What is the difference between ∀ and Π in the Calculus of Constructions?

As I've learned, the Calculus of Constructions has only two binders - $\lambda$ and $\Pi$. Morte, for example, has $\forall$ as a mere alias of $\Pi$. Yet, on the paper Self Types for Dependently ...
MaiaVictor's user avatar
  • 4,137