Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself

We describe the foundation of the metaprogramming language, Mœbius, which supports the generation of polymorphic code and, more importantly, the analysis of polymorphic code via pattern matching. Mœbius has two main ingredients: 1) we exploit contextual modal types to describe open code together with the context in which it is meaningful. In Mœbius, open code can depend on type and term variables (level 0) whose values are supplied at a later stage, as well as code variables (level 1) that stand for code templates supplied at a later stage. This leads to a multi-level modal lambda-calculus that supports System-F style polymorphism and forms the basis for polymorphic code generation. 2) we extend the multi-level modal lambda-calculus to support pattern matching on code. As pattern matching on polymorphic code may refine polymorphic type variables, we extend our type-theoretic foundation to generate and track typing constraints that arise. We also give an operational semantics and prove type preservation. Our multi-level modal foundation for Mœbius provides the appropriate abstractions for both generating and pattern matching on open code without committing to a concrete representation of variable binding and contexts. Hence, our work is a step towards building a general type-theoretic foundation for multi-staged metaprogramming that, on the one hand, enforces strong type guarantees and, on the other hand, makes it easy to generate and manipulate code. This will allow us to exploit the full potential of metaprogramming without sacrificing the reliability of and trust in the code we are producing and running.

CPS transformation with affine types for call-by-value implicit polymorphism

Transformation of programs into continuation-passing style (CPS) reveals the notion of continuations, enabling many applications such as control operators and intermediate representations in compilers. Although type preservation makes CPS transformation more beneficial, achieving type-preserving CPS transformation for implicit polymorphism with call-by-value (CBV) semantics is known to be challenging. We identify the difficulty in the problem that we call scope intrusion. To address this problem, we propose a new CPS target language Λ open that supports two additional constructs for polymorphism: one only binds and the other only generalizes type variables. Unfortunately, their unrestricted use makes Λ open unsafe due to undesired generalization of type variables. We thus equip Λ open with affine types to allow only the type-safe generalization. We then define a CPS transformation from Curry-style CBV System F to type-safe Λ open and prove that the transformation is meaning and type preserving. We also study parametricity of Λ open as it is a fundamental property of polymorphic languages and plays a key role in applications of CPS transformation. To establish parametricity, we construct a parametric, step-indexed Kripke logical relation for Λ open and prove that it satisfies the Fundamental Property as well as soundness with respect to contextual equivalence.

EMTST: Engineering the Meta-theory of Session Types

Session types provide a principled programming discipline for structured interactions. They represent a wide spectrum of type-systems for concurrency. Their type safety is thus extremely important. EMTST is a tool to aid in representing and validating theorems about session types in the Coq proof assistant. On paper, these proofs are often tricky, and error prone. In proof assistants, they are typically long and difficult to prove. In this work, we propose a library that helps validate the theory of session types calculi in proof assistants. As a case study, we study two of the most used binary session types systems: we show the impossibility of representing the first system in $$\alpha $$-equivalent representations, and we prove type preservation for the revisited system. We develop our tool in the Coq proof assistant, using locally nameless for binders and small scale reflection to simplify the handling of linear typing environments.

Soft-tissue anatomy of an Orsten-type phosphatocopid crustacean from the Cambrian Furongian of China revealed by synchrotron radiation X-ray tomographic microscopy

Fossils of Orsten-type preservation represented by Skara and Phosphatocopida have been reported from the Cambrian Furongian of Western Hunan, China. Their taxonomy and external morphology are well known, but their internal soft-tissue anatomy has not been revealed yet. With the application of synchrotron radiation X-ray tomographic microscopy, here we describe the internal soft-tissue anatomy of an Orsten-type preserved phosphatocopid crustacean assigned to Hesslandona angustata. The internal organs and tissues of this specimen were collapsed after death to form a visceral mass situated within the labrum and underneath the sternal cuticle. The visceral mass contains the digestive system, including digestive tract and possible digestive glands. The digestive tract starts from the mouth, followed by oesophagus (foregut) and midgut, whereas the hind gut and anus are unknown due to incomplete preservation. Two bilaterally symmetric knob-like structures beside the midgut may be digestive glands (midgut diverticula). The visceral mass also contains other structures that may be related to nerve tissues and/or muscles, but identification as specific organs or tissues is uncertain.

New material of scalidophoran worms in Orsten-type preservation from the Cambrian Fortunian Stage of South China

Scalidophoran worms diversified in the Cambrian Fortunian, as indicated by recent reports from this stage, with two described species and two more unnamed forms exclusively from Orsten-type Lagerstätten yielding three-dimensionally phosphatized fossils. Here, we report new material of scalidophoran worms in Orsten-type preservation from the Cambrian Fortunian Xinli section in northern Sichuan Province, South China. At least five forms of scalidophoran worms were recovered from this location, including Eokinorhynchus rarus Zhang et al., 2015 and four unnamed taxa—Forms A, B, C, and D. Co-occurring disassociated spinose small shelly fossils might also be isolated cuticular elements of these early scalidophoran worms. The ontogeny of Eokinorhynchus rarus is revised. Forms A, C, and D are assigned to total-group Scalidophora to indicate their uncertain positions within Scalidophora, while Form B might be a close relative of Eokinorhynchus rarus. The current work highlights the significance of Orsten-type Lagerstätten in uncovering the morphology, ontogeny, and taxonomy of early Scalidophora and Cycloneuralia, made particularly available by the new finds in China.