7

Since the CoC has dependent types and system $F$ does not, I'll assume you mean a function whose types is in system $F$, but whose definition can only be written in CoC. Luckily in this case we can restrict to system $F_\omega$, which can express the same non-dependent functions as CoC, by some erasure argument. In general, a rule of thumb to construct such ...


6

The discussion in the section surrounding that paragraph in Pierce's book explains why this is so. In particular, consider the definition of "type system" given on the page before: A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute. ...


6

The standard well-formed-related predicate can be relatively easily extended to handle untyped PHOAS. The main subtlety is how to handle reduction at the type level. Here's a start of a two-place relation for well-typed in Coq: Require Import Coq.Lists.List. Reserved Infix "@" (left associativity, at level 11). Local Open Scope list_scope. Inductive expr ...


4

This isn't an excessively deep answer, but you can express a type system based on STLC with prenex polymorphism as a Pure Type System in a quite simple way, using sorts $*_{\mathrm{mono}}$, $*_{\mathrm{poly}}$ and $\square$ along with the axioms $$ *_{\mathrm{mono}}, *_{\mathrm{poly}}\ :\ \square$$ and the rules $$(*_{\mathrm{mono}},*_{\mathrm{mono}},*_{\...


4

Apart from what's already written in the slides you linked to, let me describe one possible approach. For studying type inference semantically we need a model in which a term can have many types, or none. This naturally leads to Curry-style typing, i.e., we think of $t : A$ as a relation where both the term $t$ and the type $A$ are meaningful by themselves. (...


4

The point of stacks is that they are in a sense the dual concept to computations. A computation does not run in a vacuum. It is always "surrounded" by some sort of an environment, or evaluation context, telling us what the current "state of progress" is, or is recording "where we are, and where we're going". Often this sort of information has stack-like ...


3

Since Andrej has somewhat covered the operational side, I'll take the more semantic/category theoretic perspective of why we care about stacks, that is especially relevant in EEC. The general philosophy of categorical logic is that all types should be defined by a universal property. In CBPV without stacks, you cannot give a universal property to the $F$ ...


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