Formalizing semantic bidirectionalization and extensions with dependent types

DOI10.1016/j.jlamp.2016.04.002zbMath1353.68042OpenAlexW2473813316MaRDI QIDQ347391

Janis Voigtländer, Helmut Grohne

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

formal verificationdependent typesAgdabidirectional programming

Mathematics Subject Classification ID

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

Uses Software

• Agda
• PoplMark

Cites Work

• Unnamed Item
• A programmable editor for developing structured documents based on bidirectional transformations
• Proofs for free
• Applicative bidirectional programming with lenses
• Dependently Typed Programming in Agda
• Update semantics of relational views
• Three Complementary Approaches to Bidirectional Programming
• Transporting functions across ornaments
• Bidirectionalization transformation based on automatic derivation of view complement functions
• Bidirectionalizing graph transformations
• Type-theory in color
• Bidirectionalization for free! (Pearl)
• A Categorical Treatment of Ornaments
• Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins
• Theorem Proving in Higher Order Logics