Questions tagged [types-and-programming-languages]

For questions about the book "Types and Programming Languages" by Benjamin Pierce, and the exercises from the book.

10 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
6 votes
0 answers
106 views

Bounded existential polymorphism

In his "Types and Programming Languages", Pierce, at the very end, presents the most powerful system in the book: $F^{\omega}_{<:}$. He, however, does not explain how bounded existential ...
Jake's user avatar
  • 3,810
3 votes
0 answers
55 views

On the diamond property for $F_{\omega}$ in TAPL

In page 455, of Pierce´s TAPL and page 560, the single-step diamond property of reduction: $S \Rrightarrow S' \land T \Rrightarrow T' \implies \exists V. T \Rrightarrow V \land U \Rrightarrow V$ ...
user1868607's user avatar
  • 2,194
2 votes
0 answers
100 views

Are the permutation or weakening lemmas needed for term substitution?

In TAPL book, page 453, Pierce discusses the following lemma: $\Gamma , x:S , \Delta \vdash t:T \land \Gamma \vdash s:S \implies \Gamma, \Delta \vdash [x \mapsto s]t:T$ He claims that when $t$ is ...
user1868607's user avatar
  • 2,194
2 votes
0 answers
108 views

Is the language "untyped arithmetic expressions" in Types and Programming Languages not Turing complete?

In Types and Programming Languages by Pierce, is it correct that the language introduced in Chapter 3 Untyped Arithmetic Expressions is not Turing complete? Because it doesn't provide recursion. the ...
Tim's user avatar
  • 4,895
2 votes
0 answers
40 views

Region-based memory management for recursive type

In the chapter 4 of Pierce's TAPL which discusses the implementation of untyped arithmetic expressions, the author said The most important [for the implementation requirements] are automatic ...
Ta Thanh Dinh's user avatar
1 vote
0 answers
34 views

What logical system does hindley-milner correspond to, according to the curry howard correspondence?

If I understand CHC correctly, simply typed lambda calculus corresponds to propositional logic. As HM allows polymorphic definitions by let-expressions, my guess is that it would correspond to a ...
pgmcr's user avatar
  • 36
1 vote
0 answers
80 views

The abstract interpretation corresponding to the pure simply typed lambda calculus

In Types as Abstract Interpretation, Patrick Cousot sketched how different type systems could be constructed from the collecting semantics of a language. However, the notation of the paper is very old ...
user1868607's user avatar
  • 2,194
1 vote
0 answers
48 views

How does progress fail in system $F_{\omega}$ when types $T_1 \to T_2$ and $T_2 \to T_1$ are equivalent?

Pierce's TAPL book gives in exercise 30.3.17 the setting where $T_1 \to T_2 \equiv T_2 \to T_1$ (the function type are assumed to be equivalent). In the solutions, he claims that this assumption ...
user1868607's user avatar
  • 2,194
1 vote
0 answers
79 views

Mathematical resource material accompanying TAPL

I'm currently reading Types and Programming Languages by Benjamin C. Pierce and just arrived at chapter 21 Metatheory of Recursive Types. Prior to this chapter I found the book challenging but ...
needstolearnmath's user avatar
0 votes
0 answers
78 views

Semantics Equivalence of Structural Semantics of While Programming Language

I'm taking a course about the formality of programming languages and while reading Semantics with Applications: An Appetizer by H.R Nielson and F. Nielson I came across the following exercise: I'm ...
MiddleEasternPrince's user avatar