14 votes

Where is the model theory in programming language theory?

Let me amend Damiano's answer with more specific comments. Terms of type bool are not logical statements. Expressions like ...
Andrej Bauer's user avatar
  • 28.7k
13 votes
Accepted

Where is the model theory in programming language theory?

The model theory of programming languages is called denotational semantics. You can google the term to find out more about it, I'll give an extreme synthesis of it. Denotational semantics is a ...
Damiano Mazza's user avatar
10 votes

Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic

I do not know if this answers your question, but in Propositions as [Types] we communicate in Remark 6.6 an observation by Thierry Coquand, namely that the statement $$ (\forall x .\, \exists y .\, R(...
Andrej Bauer's user avatar
  • 28.7k
9 votes

Example of a term in system F which is not typable in the simply typed lambda calculus

Reacting to the previous answers, I think this is the simplest self-application which only contains types which have closed inhabitants. $$\lambda\,(f\,:\,\forall\,\alpha.\,\alpha\to\alpha).\,f\,(\...
András Kovács's user avatar
7 votes

Example of a term in system F which is not typable in the simply typed lambda calculus

Damiano Mazza's example uses an uninhabited type, $∀ X ⋅ X$. It is correct, but raises the obvious question whether one can do without. Here is an example that I find quite natural: $$Λ \ A B ⋅ λ \ (p ...
Jean Abou Samra's user avatar
7 votes
Accepted

Example of a term in system F which is not typable in the simply typed lambda calculus

Every normal term may be typed in system F (I can't seem to find a reference now, I'll come back with one when I have some more time). So, for example, letting $A:=\forall X.X$, then $$x^A(A\to\alpha)...
Damiano Mazza's user avatar
6 votes
Accepted

Formulation of Tarski-style universes in LF

Papers on universes are usually concerned with universes that are large, i.e., most authors are intersted only in universes closed under dependent products. But nothing prevents us from having a baby ...
Andrej Bauer's user avatar
  • 28.7k
5 votes
Accepted

Power of existential types

Universal types can be used to encode the least fixed point, while dually, existential types can be used to encode the greatest fixed point. For example, consider $F(X) = 1 + A \times X$, then the ...
Trebor's user avatar
  • 335
5 votes
Accepted

Generalizations, or extensions of W-types in MLTT

The representation issue of W-types was resolved by Jasper Hugunin. So from type formers $0$, $1$, $2$, $W$, $\Pi$, $\Sigma$, identity and a universe hierarchy we do get all indexed inductive families ...
András Kovács's user avatar
4 votes
Accepted

Is Linear Evaluation Parametric?

Here's an Agda formalization of the non-linear version of your argument, and my comment above: ...
Dan Doel's user avatar
  • 931
3 votes
Accepted

Is is true that every monad transformer is equivalent to its underlying/base monad?

The equation F Id ≅ ∀ (m: Monad). F m seems to be correct (for most transformers F, see below). However, I would not say that &...
winitzki's user avatar
  • 294
3 votes

Generalizations, or extensions of W-types in MLTT

You could start with Spartan type theory (which honestly should be upgraded to use evaluation-by-normalization) and add simple inductive datatypes to them. This would involve several steps. First, add ...
Andrej Bauer's user avatar
  • 28.7k
3 votes
Accepted

Is there an efficient algorithm to check for duplicator-invariant equivalence on symmetric interaction combinators?

This does not answer your main question but concerns the following point: I'm looking for an equivalence on interaction nets that implies lambda calculus read-back equivalence, but that also ...
Damiano Mazza's user avatar
2 votes

Derivability of `Vector` in pure calculus of constructions

Source 1 does not say anything about deriving the induction principle for inductive types, it's only about non-dependent recursion. Source 2 says that deriving the induction principle is not possible. ...
András Kovács's user avatar
2 votes

Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?

I claim that $T \cong \mathbb 1+\mathbb2+\mathbb3\,+\,…$. I will prove the type equivalence and then show what terms of type $T$ correspond to values of type $\mathbb 1+\mathbb2+\mathbb3\,+\,…$ The ...
winitzki's user avatar
  • 294
2 votes
Accepted

Type of the Recursor in Lean

Ok, let's try to unpack this a bit. Basically we are trying to define a recursor for a very general inductive datatype in a very complex type theory, with dependent types, universes and ...
cody's user avatar
  • 13.8k
2 votes
Accepted

Intuition behind UTT's internal logic

$\mathit{Prop}$ is a universe and $\mathrm{Prf}$ is its decoding function. (Often called $T$ for Tarski-style universe.) $\Lambda$ is the introduction rule for universal quantification. $\mathbf{E}_\...
Andrej Bauer's user avatar
  • 28.7k
2 votes

Where is the model theory in programming language theory?

Models in some semantic framework are essentially a mapping from synthetic objects to some other domain of object. In the sematic domain we typically identify or take as equivalent a bunch of ...
Kaveh's user avatar
  • 21.6k
2 votes
Accepted

Denotational semantics of intersection types

Intersection types appear in typed programming languages to capture the idea that a given expression may carry multiple functionalities. For example, given a type $\mathsf{read}\;\alpha$ of readable ...
Andrej Bauer's user avatar
  • 28.7k
2 votes

Denotational semantics of intersection types

Later edit: When I wrote the answer below, I was thinking of intersection types as they are understood in the context of the untyped $\lambda$-calculus. It is now clear that this is not the right ...
Damiano Mazza's user avatar
2 votes
Accepted

Can you regain the Church-Rosser property in languages with continuations?

A simple fix is to add call-by-value let-expressions$$\text{let } x := t\text{ in }u$$that evaluate $t$ to a value and then substitute it for $x$. Having these in the language allows to restrict $+$ ...
xavierm02's user avatar
  • 556
1 vote

How is runtime downcasting modeled in type theory?

For type theory of object oriented programming, see [1]. There are many models for object oriented programming language concepts. Often type theory of OO is expressed in terms of category theory for ...
Esa Pulkkinen's user avatar
1 vote

Where is the model theory in programming language theory?

Thanks to everyone! I'm just going to summarize my takeaway from the helpful responses and comments above targeted towards someone in mathematical logic wondering the same thing as I did. Please let ...
Siddharth's user avatar
  • 823
1 vote

What is the relation of parametricity and function extensionality?

Indeed there is a similarity in these two definitions. Function extensionality that you showed is just a condition that specifies when two functions are equal. If we talk about logical relations then ...
winitzki's user avatar
  • 294

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