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

Dependently-typed host languages empower users to verify a wide range ofproperties of embedded languages and programs written in them. Designers ofsuch embedded languages are faced with a difficult choice between using ashallow or a deep embedding. The former is easier to use because the entireinfrastructure of the host langauge is immediately available. Meanwhile, thelatter gives full access to the structure of embedded programs, but isdifficult to use in practice, especially when the embedded language is itselfdependently typed.  The main insight presented in this paper is that the choice between shallowand deep embedding can be eliminated by working in a host language withreflection capabilities: we start from a shallow embedding that can use alllibraries and tools of the host language, and later use reflection to exposethe deep structure of the embedded programs.  Concretely, we apply this technique to embed three programming languages --Kaleidoscope, SaC, and (a subset of) APL -- into the dependently typed theoremprover Agda, using dependent types to statically enforce several properties ofinterest. We then use Agda's reflection capabilities to extract the embeddedprograms back into the original language, so that the existing toolchain can beleveraged.  In this process, statically verified properties of the host language aremapped onto runtime checks in the target language, allowing extracted programsto interact safely with existing code.  Finally, we demonstrate the feasibility of our approach with theimplementation and extraction of a convolutional neural network in ourembedding of APL.\@

Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection