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.

Formal metatheory of second-order abstract syntax

Despite extensive research both on the theoretical and practical fronts, formalising, reasoning about, and implementing languages with variable binding is still a daunting endeavour – repetitive boilerplate and the overly complicated metatheory of capture-avoiding substitution often get in the way of progressing on to the actually interesting properties of a language. Existing developments offer some relief, however at the expense of inconvenient and error-prone term encodings and lack of formal foundations. We present a mathematically-inspired language-formalisation framework implemented in Agda. The system translates the description of a syntax signature with variable-binding operators into an intrinsically-encoded, inductive data type equipped with syntactic operations such as weakening and substitution, along with their correctness properties. The generated metatheory further incorporates metavariables and their associated operation of metasubstitution, which enables second-order equational/rewriting reasoning. The underlying mathematical foundation of the framework – initial algebra semantics – derives compositional interpretations of languages into their models satisfying the semantic substitution lemma by construction.

Modeling the dynamics of within-host viral infection and evolution predicts quasispecies distributions and phase boundaries separating distinct classes of infections

We use computational modeling to study within-host viral infection and evolution. In our model, viruses exhibit variable binding to cells, with better infection and replication countered by a stronger immune response and a high rate of mutation. By varying host conditions (permissivity to viral entry T and immune clearance intensity A) for large numbers of cells and viruses, we study the dynamics of how viral populations evolve from initial infection to steady state and obtain a phase diagram of the range of cell and viral responses. We find three distinct replicative strategies corresponding to three physiological classes of viral infections: acute, chronic, and opportunistic. We show similarities between our findings and the behavior of real viral infections such as common flu, hepatitis, and SARS-CoV-2019. The phases associated with the three strategies are separated by a phase transition of primarily first order, in addition to a crossover region. Our simulations also reveal a wide range of physical phenomena, including metastable states, periodicity, and glassy dynamics. Lastly, our results suggest that the resolution of acute viral disease in patients whose immunity cannot be boosted can only be achieved by significant inhibition of viral infection and replication.

Locative Inversion, PP Topicalization, and Weak Crossover in English

The literature on locative inversion in English currently disputes whether locative inversion differs from PP topicalization in permitting a quantifier in the fronted PP to bind a pronoun in the subject. In order to resolve this dispute, this paper runs two experiments on Amazon Mechanical Turk, one an acceptability judgment task and the other a forced-choice task. Both find that PP topicalization does not differ from locative inversion: both permit variable binding. Locative inversion also does not differ from a minimally different sentence with the overt expletive there. These findings remove an argument against the null expletive analysis of English locative inversion, and they also show that weak crossover is not uniformly triggered by A-bar movement.

Abstraction Logic

Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-order logic and second-order logic. It is sound with respect to an intuitive and simple algebraic semantics. Completeness holds for both intuitionistic and classical abstraction logic, and all abstraction logics in between and beyond.

Abstraction Logic

Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-order logic and second-order logic. It is sound and complete with respect to an intuitive and simple algebraic semantics.

Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)

Rigorous reasoning about programs calls for some amount of bureaucracy in managing details like variable binding, but, in guiding students through big ideas in semantics, we might hope to minimize the overhead. We describe our experiment introducing a range of such ideas, using the Coq proof assistant, without any explicit representation of variables, instead using a higher-order syntax encoding that we dub "mixed embedding": it is neither the fully explicit syntax of deep embeddings nor the syntax-free programming of shallow embeddings. Marquee examples include different takes on concurrency reasoning, including in the traditions of model checking (partial-order reduction), program logics (concurrent separation logic), and type checking (session types) -- all presented without any side conditions on variables.

Deriving efficient program transformations from rewrite rules

An efficient optimizing compiler can perform many cascading rewrites in a single pass, using auxiliary data structures such as variable binding maps, delayed substitutions, and occurrence counts. Such optimizers often perform transformations according to relatively simple rewrite rules, but the subtle interactions between the data structures needed for efficiency make them tricky to write and trickier to prove correct. We present a system for semi-automatically deriving both an efficient program transformation and its correctness proof from a list of rewrite rules and specifications of the auxiliary data structures it requires. Dependent types ensure that the holes left behind by our system (for the user to fill in) are filled in correctly, allowing the user low-level control over the implementation without having to worry about getting it wrong. We implemented our system in Coq (though it could be implemented in other logics as well), and used it to write optimization passes that perform uncurrying, inlining, dead code elimination, and static evaluation of case expressions and record projections. The generated implementations are sometimes faster, and at most 40% slower, than hand-written counterparts on a small set of benchmarks; in some cases, they require significantly less code to write and prove correct.

Caffeine Interactions with Wood Polymers

Caffeine is a verified bioactive substance suitable for wood protection against pests. Unlike studies of the biocidal effects of caffeine, caffeine-wood bonds and interactions with wood polymer structures have not been studied whatsoever thus far. For this reason, caffeine (1 g/L) interactions with the main wood components (cellulose; hemicellulose; lignin and its precursors conipheryl alcohol, sinapyl alcohol, coumaryl alcohol) were analyzed in the present study. Caffeine concentrations were analyzed using UV–VIS spectrometry at wavelength 287 nm. The results confirmed caffeine variable binding with wood components in comparison to controls (pure caffeine). Cellulose and sinapyl alcohol did not interact with caffeine. Caffeine was bonded with the rest of the wood components in an increasing rank: conipheryl alcohol = lignin < hemicellulose < coumaryl alcohol. These results have a significant role in the protection of wood depending on its chemical composition and the wood species.

Encephalitis patient derived monoclonal GABAA receptor antibodies cause catatonia and epileptic seizures

Autoantibodies targeting the GABAA receptor (GABAAR) hallmark an autoimmune encephalitis presenting with frequent seizures and psychomotor abnormalities. Their pathogenic role is still not well-defined, given the common overlap with further autoantibodies and the lack of patient derived monoclonal antibodies (mAbs). We cloned and recombinantly produced five affinity-maturated GABAAR IgG1 mAbs from cerebrospinal fluid cells, which bound to various epitopes involving α1 and γ2 receptor subunits, with variable binding strength and partial competition. mAbs selectively reduced GABAergic currents in neuronal cultures without causing receptor internalization. Cerebroventricular infusion of GABAAR mAbs and Fab fragments into rodents induced a severe phenotype with catatonia, seizures and increased mortality, reminiscent of encephalitis patients’ symptoms. Our results prove direct functional effects of autoantibodies on GABAARs and provide an animal model for GABAAR encephalitis. They further provide the scientific rationale for clinical treatments using antibody depletion and pave the way for future antibody-selective immunotherapies.