English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We describe the foundation of the metaprogramming language, Moebius, whichsupports the generation of polymorphic code and, more importantly the analysisof polymorphic code via pattern matching.  Moebius has two main ingredients: 1) we exploit contextual modal types todescribe open code together with the context in which it is meaningful. InMoebius, open code can depend on type and term variables (level 0) whose valuesare supplied at a later stage, as well as code variables (level 1) that standfor code templates supplied at a later stage. This leads to a multi-level modallambda-calculus that supports System-F style polymorphism and forms the basisfor polymorphic code generation. 2) we extend the multi-level modallambda-calculus to support pattern matching on code. As pattern matching onpolymorphic code may refine polymorphic type variables, we extend ourtype-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 Moebius provides the appropriateabstractions for both generating and pattern matching on open code withoutcommitting to a concrete representation of variable binding and contexts.Hence, our work is a step towards building a general type-theoretic foundationfor multi-staged metaprogramming that, on the one hand, enforces strong typeguarantees and, on the other hand, makes it easy to generate and manipulatecode. This will allow us to exploit the full potential of metaprogrammingwithout sacrificing the reliability of and trust in the code we are producingand running.

Moebius: Metaprogramming using Contextual Types -- The stage where System F can pattern match on itself (Long Version)