Formalizing semantic bidirectionalization and extensions with dependent types

DOI10.1016/J.JLAMP.2016.04.002MaRDI QIDQ347391zbMATH OpenOpenAlexFDO

Authors Helmut Grohne, Janis Voigtländer

Publication date 30 November 2016

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2016.04.002

zbMATH Keywords

Agdadependent typesformal verificationbidirectional programming

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Recommendations

• Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins
• Bidirectionalization for free! (Pearl)
• Bidirectionalization transformation based on automatic derivation of view complement functions
• Applicative bidirectional programming with lenses
• Combining syntactic and semantic bidirectionalization

Cites work

• scientific article; zbMATH DE number 1956503 (Why is no real title available?)
• A Categorical Treatment of Ornaments
• A programmable editor for developing structured documents based on bidirectional transformations
• Applicative bidirectional programming with lenses
• Bidirectionalization for free! (Pearl)
• Bidirectionalization transformation based on automatic derivation of view complement functions
• Bidirectionalizing graph transformations
• Dependently typed programming in Agda
• Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins
• Proofs for free. Parametricity for dependent types
• Theorem Proving in Higher Order Logics
• Three complementary approaches to bidirectional programming
• Transporting functions across ornaments
• Type-theory in color
• Update semantics of relational views

Cited in

(3)

• Composing bidirectional programs monadically
• Extensional and Intensional Semantic Universes
• Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins

Describes a project that uses

Uses Software

• PoplMark
• Agda

This page was built for publication: Formalizing semantic bidirectionalization and extensions with dependent types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q347391)