ABSTRACT. We give an overview of the theory and practice of second-order rewriting. Second-order rewriting methods have been demonstrated as useful that is applicable to important notions of programming languages such as logic programming, algebraic effects, quantum computation, and cyclic computation. We explain foundation and evolution of second-order rewriting by presenting the framework of polymorphic second-order computation systems. We also demonstrate our system SOL of second-order laboratory through various programming language examples.

ABSTRACT. Call-by-Push-Value (CBPV) is a programming paradigm subsuming both Call-by-Name (CBN) and Call-by-Value (CBV) semantics. The paradigm was recently modelled by means of the Bang Calculus, a term language connecting CBPV and Linear Logic.

This paper presents a revisited version of the Bang Calculus, called lambda!, enjoying some important properties missing in the original system. Indeed, the new calculus integrates commutative conversions to unblock value redexes while being confluent at the same time. A second contribution is related to non-idempotent types. We provide a quantitative type system for our lambda!-calculus, and we show that the length of the (weak) reduction of a typed term to its normal form "plus" the size of its normal form is bounded by the size of its type derivation. We also explore the properties of this type system with respect to CBN/CBV translations. We keep the original CBN translation from lambda-calculus to the Bang Calculus, which preserves normal forms and is sound and complete with respect to the (quantitative) type system for CBN. However, in the case of CBV, we reformulate both the translation and the typing system to restore two main properties: preservation of normal forms and completeness. Last but not least, the quantitative system is refined to a "tight" one, which transforms the previous "upper bound" on the length of reduction to normal form plus its size into two independent "exact measures" for them.

ABSTRACT. Abstract. We introduce a simple untyped extensions of the λ-calculus with pairs—called the distributive λ-calculus—with rules to commute pairs with applications, and abstractions with projections. Key features are confluence, the absence of clashes of constructs, that is, evaluation never gets stuck, and a leftmost-outermost normalization theorem, obtained with straightforward proofs. We then add simple types, and show that the new rules satisfy subject reduction if types are considered up to the distributivity isomorphism A → (B ∧ C) ≡ (A → B) ∧ (A → C), that is a valid isomorphism of simple types. The main result is strong normalization for simple types up to distributivity. The proof is a smooth variation over the one for the λ-calculus with pairs and simple types.

ABSTRACT. To demonstrate derivation of monadic programs, we present a specification of sorting using non-determinism monad, and derive pure quicksort on lists and state-monadic quicksort on arrays. In the derivation one may switch between point-free and pointwise styles, and deploy techniques familiar to functional programmers such as pattern matching and induction on structures or on sizes. Derivation of stateful programs resembles reasoning backwards from the postcondition.