Programming with ornaments

DOI10.1017/S0956796816000307MaRDI QIDQ5372000zbMATH OpenFDO

Authors Hsiang-Shang Ko, Jeremy Gibbons

Publication date 23 October 2017

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0956796816000307

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• The essence of ornaments
• A Categorical Treatment of Ornaments
• Transporting functions across ornaments
• Transporting functions across ornaments
• Refining inductive types

Cites work

• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• Advanced functional programming. 6th international school, AFP 2008, Heijen, The Netherlands, May 2008. Revised lectures
• Dependent Types at Work
• Eliminating Dependent Pattern Matching
• How to keep your neighbours in order
• Inductive families
• On the bright side of type classes: instance arguments in Agda
• Pattern matching without K
• Programming in Ωmega
• Purely Functional Data Structures
• The gentle art of levitation
• The view from the left
• Transporting functions across ornaments
• Type-theory in color
• Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 -- May 4, 2003. Revised selected papers.

Cited in

(7)

• Heterogeneous binary random-access lists
• Transporting functions across ornaments
• Calculating datastructures
• The essence of ornaments
• scientific article; zbMATH DE number 638307 (Why is no real title available?)
• Ornaments for Proof Reuse in Coq
• Transporting functions across ornaments

Describes a project that uses

Uses Software

• Agda

This page was built for publication: Programming with ornaments

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