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

In terms of related work, Marek Zaionc and collaborators have been studying similar kinds of questions for some time. The following paper includes many results: René David, Katarzyna Grygiel, Jakub Kozic, Christophe Raffalli, Guillaume Theyssier, Marek Zaionc. Asymptotically almost all λ-terms are strongly normalizing. Logical Methods in Computer Science,...


5

There are no metrics, but an excellent discussion of many concurrency models, in Tony Garnock-Jones PhD thesis. See the (HTML version of the) chapter "Approaches to coordination". This studies concurrency models with a particular focus, namely how information is exchanged for coordination.


5

$\beta(E_1)$ is the language $s^nx,s^{n+1}x$. This language is straightforwardly not regular, by the pumping lemma. If we assume that the language is regular, the pumping lemma tells us that there must exist some $p, q$ such that for all $n \ge p$, $s^{n+q}x,s^{n+1}x$ is also in the language. This is false, meaning that the language is not regular. A similar ...


5

This is just a long comment (too many words to fit in a comment box). Gérard Huet is, among other things, an expert in $\lambda$-calculus who worked worked a lot on the computational processing of Sanskrit, including its phonological aspects. I remember him once giving a talk in Marseilles entitled Des Lambdas et des Aums ("Lambdas and Oms") but ...


5

Let's look at a simple example of a toy programming language with unary natural numbers and a "predecessor" operation. $$t ::= 0 \mid S~t \mid p~t$$ whose semantics is given by the following rewrite rules $$p~(S~t) \to t \qquad p~0 \to 0$$ with $$\mathsf{size}(0) = 1 \qquad \mathsf{size}(S~t) = 1 + \mathsf{size}(t) \qquad \mathsf{size}(p~t) = 1 + \...


5

This question is very open-ended and therefore difficult to answer, but I think the short answer is "yes", there is much common ground, the two areas have in fact benefited from interaction in the past, and they have much to gain from further interaction. Two classical examples of this (respectively from the 1950s and '70s) are Lambek grammar and ...


5

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}},*_{\...


5

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. (...


3

This is the notation for Harper's "abstract binding structures": x.t represents the binding site of a variable x and the term t the variable scopes over. Apparently you are in the parts that define variable bindings. $\mathcal{B}[\mathcal{X}]_s$ appears to be the set of terms, or binding structures at sort $s$ whose free variables are among $\...


2

It is. There's a fairly simple construction compiling from CT to CT2. First, consider that it's possible to double every command in a CT program without producing any behaviour (that is, A becomes AA, B becomes BB, C becomes CC). The queue of bits now has every bit doubled, but the cycle of commands only does anything with every second bit, so the modified ...


1

Here is an example exploiting positivity of an index to prove false: module Whatever where open import Level using (Level) open import Relation.Binary.PropositionalEquality open import Data.Empty variable ℓ : Level A B : Set ℓ data _≅_ (A : Set ℓ) : Set ℓ → Set ℓ where trefl : A ≅ A Subst : (P : Set ℓ → Set ℓ) → A ≅ B → P A → P B Subst P trefl PA = ...


1

Milner defines the SCCS calculus in [1]. This is a generalization of CCS where the actions form an abelian group, and where the communication rule is defined as in my question. [1] Milner, R. Calculi for synchrony and asynchrony. 1983. https://www.sciencedirect.com/science/article/pii/0304397583901147


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