Data structures and program transformation
From MaRDI portal
An extension of the Bird-Meertens formalism for program transformations to arbitrary data types is proposed. The approach is based on the notion of initial data types. The construction of structure-preserving maps is described and a promotion theorem for proving their equalities is derived. Examples include tree structures and infinite lists.
Recommendations
Cited in
(42)- Datatype-generic termination proofs
- A `division' transformation for program and data structures and the structure clash problem
- Inductive data types for predicate transformers
- Paramorphisms
- Calculate categorically!
- The derivation of on-line algorithms, with an application to finding palindromes
- Polytypic data conversion programs
- A hidden agenda
- Generic recursive lens combinators and their calculation laws
- Recursive coalgebras from comonads
- Data structures of programming languages as realization of the nominative data
- Strongly typed rewriting for coupled software transformation
- scientific article; zbMATH DE number 2084336 (Why is no real title available?)
- Factorising folds for faster functions
- scientific article; zbMATH DE number 3845032 (Why is no real title available?)
- ``Everything is everything revisited: shapeshifting data types with isomorphisms and hylomorphisms
- A Groupoid of Isomorphic Data Transformations
- From Coinductive Proofs to Exact Real Arithmetic
- Libraries for generic programming in Haskell
- scientific article; zbMATH DE number 3970091 (Why is no real title available?)
- The Mechanical Transformation of Data Types
- Categories, relations and dynamic programming
- Set notation as a language to specify data transformation programs
- Generic functional programming with types and relations
- Datatype laws without signatures
- Process Calculi à la Bird-Meertens
- When is a function a fold or an unfold?
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Categorical fixed point calculus
- POPLMark reloaded: mechanizing proofs by logical relations
- Unifying structured recursion schemes. An extended study
- Programming Languages and Systems
- Fusion of recursive programs with computational effects
- Least and greatest fixed points in intuitionistic natural deduction
- Constructing language processors with algebra combinators
- Folding over neural networks
- Classical (co)recursion: Mechanics
- Fantastic morphisms and where to find them. A guide to recursion schemes
- Algebraic dynamical systems in machine learning
- Isomorphic data type transformations
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- The formalism underlying EASYMAP: A precompiler for refinement-based exploration of hierarchical data organizations
This page was built for publication: Data structures and program transformation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q749197)
