# Questions tagged [type-theory]

Type structure is a syntactic discipline for enforcing levels of abstraction.

268 questions
Filter by
Sorted by
Tagged with
171 views

### Eta expansion in the pattern lambda calculus

Klop, van Oostrom, and de Vrijer have a paper on the lambda calculus with patterns. http://www.sciencedirect.com/science/article/pii/S0304397508000571 In some sense, a pattern is a tree of variables ...
298 views

### Proving running time upper bounds for algorithms in dependent type theory

Proof assistants are a valuable tool for verifying the correctness of proofs of mathematical theorems. When dealing with proofs of correctness of algorithms, one is not only interested on showing ...
457 views

### What is the intuition behind linear logic?

I'm trying to understand linear logic to understand linear type systems better. However, when I read the rules, I fail to get an intuition behind it as I've done in modal logic - $\Box A$ means $A$ is ...
426 views

### Wouldn't the calculus of constructions with linear types be a simple functional core that is consistent and expressive?

I have recently asked if there is a simple functional core that is consistent and expressive. In another question, cody pointed out that this is an open problem to have a language that is: Consistent/...
1k views

### What kind of theoretical object corresponds to a C++ concept?

I am lacking a background in theoretical computer science but I would have liked to understand to what kind of theoretical objects C++ concepts corresponds to. Basically, C++ concepts allow to define ...
84 views

### Completeness of Constraint Typing (type inference) question regarding $\sigma'$

The theorem of completeness of type inference states the following: Suppose $\Gamma \vdash t:S| _{\mathcal{X}}C$, ...
143 views

### Relationship between Pataraia's theorem and inductive-recursive definitions?

Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem ...
140 views

### What's the definition of join on iso-recursive types?

In languages with subtyping, there is often a "join" operation defined to compute the least upper bound of two types. It's used in type-checking, for example to find the smallest type that covers both ...
407 views

### Determinism and pi-calculus

Milner embedded $\lambda$-calculus into $\pi$-calculus, showing that the $\pi$-calculus is capable of Turing-complete, deterministic calculation. Since parallel compositions of processes in the $\pi$-...
72 views

### Coherence spaces and full completeness for the implicative fragment of linear logic

Linear logic isn't complete for coherence space semantics since $1$ and $\top$ get identified. But it is, I believe, complete for the fragment of linear logic whose only connective is $\multimap$. I ...
300 views

### Are there simple core languages which are consistent and expressive?

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
161 views

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

What is the proof that the calculus of constructions, extended with recursive types (i.e., Fix at the type-level) isn't strongly normalizing?
132 views

### How to mechanically derive the recursor of a type from its constructors?

In Martin-Löf Dependent Type Theory a type is commonly prescribed by how to construct its canonical terms and how to show that its canonical terms are definitionally equal. This means that the ...
708 views

### Does the Law of Excluded Middle imply the Axiom K in Martin-Löf's Intensional Type Theory?

So I've been wondering if the Law of Excluded Middle (LEM) implies the so-called Axiom K in Martin-Löf's Intensional Type Theory. The Axiom K states that \Pi_{A : Type} \Pi_{x : A} \Pi_{p : \text{Id}...
636 views

### For what languages is there already a theory of observational equivalence?

For a correctness proof, I'm looking for a usable notion of program equivalence $\cong$ for Barendregt's pure type systems (PTSs); missing that, for enough specific type systems. My goal is simply to ...
623 views

### “Impredicative” in type theory

I am confused. I think I've read two usages of the word "impredicative" in type theory: When people talk about the "impredicative" version of Martin-Löf's type theory, which they say it is ...
823 views

### Law of excluded middle in MLTT

Is it possible to add law of excluded middle to Martin-Löf type theory as an axiom? It seems to me, that it's possible to add it to Coq since Coq has a module for non-constructive reasoning. Also, it ...
460 views

387 views

### Examples of Universe inconsistency in normal use of dependent types

In dependent types, Type : Type results in inconsistency (Girard's or Hurken's paradox). Are there examples of universe inconsistency (where assuming ...
357 views

### PiSigma: why does 'unfold' bind a variable?

I'm trying to understand the paper ΠΣ: Dependent Types without the Sugar by implementing an interpreter and type checker for the language. In doing so, I've seen that the ...