Arrow Research search

Author name cluster

Peter Thiemann

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers
1 author row

Possible papers

2

I&C Journal 2022 Journal Article

Polymorphic lambda calculus with context-free session types

  • Bernardo Almeida
  • Andreia Mordido
  • Peter Thiemann
  • Vasco T. Vasconcelos

Session types provide a typing discipline for structured communication on bidirectional channels. Context-free session types overcome the restriction to tail recursive protocols characteristic of conventional session types. This extension enables the serialization and deserialization of tree structures in a fully type-safe manner. We present the theory underlying the language FreeST 2, which features context-free session types in an extension of System F with linear types and a kinding system to distinguish message types, session types, and channel types. The system presents metatheoretical challenges which we address: contractivity in the presence of polymorphism, a non-trivial equational theory on types, and decidability of type equivalence. We also establish standard results on typing preservation, progress, and a characterization of erroneous processes.

Details DOI

I&C Journal 2002 Journal Article

Syntactic Type Soundness Results for the Region Calculus

  • Cristiano Calcagno
  • Simon Helsen
  • Peter Thiemann

The region calculus of Tofte and Talpin is a polymorphically typed lambda calculus with annotations that make memory allocation and deallocation explicit. It is intended as an intermediate language for implementing Hindley-Milner typed functional languages such as ML without traditional trace-based garbage collection. Static region and effect inference can be used to annotate a statically typed ML program with memory management primitives. Soundness of the calculus with respect to the region and effect system is crucial to guarantee safe deallocation of regions, i. e. , deallocation should only take place for objects which are provably dead. The original soundness proof by Tofte and Talpin requires a complex co-inductive safety relation. In this paper, we present two small-step operational semantics for the region calculus and prove their type soundness with respect to the region and effect system. Following the standard syntactic approach of Wright, Felleisen, and Harper, we obtain simple inductive proofs. The first semantics is store-less. It is simple and elegant and gives rise to perspicuous proofs. The second semantics provides a store-based model for the region calculus. Albeit slightly more complicated, its additional expressiveness allows us to model operations on references with destructive update. A pure fragment of both small-step semantics is then proven equivalent to the original big-step operational approach of Tofte and Talpin. This leads to an alternative soundness proof for their evaluation-style formulation.

Details DOI
v2026.09.13