The essence of ornaments

DOI10.1017/S0956796816000356MaRDI QIDQ5372005zbMATH OpenOpenAlexFDO

Authors Pierre-Évariste Dagand

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/s0956796816000356

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65)

Recommendations

• A Categorical Treatment of Ornaments
• Programming with 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?)
• scientific article; zbMATH DE number 3750146 (Why is no real title available?)
• scientific article; zbMATH DE number 2182485 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• A Categorical Treatment of Ornaments
• A UNIVERSE OF STRICTLY POSITIVE FAMILIES
• A set constructor for inductive sets in Martin-Löf's type theory
• Complete and decidable type inference for GADTs
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Indexed containers
• Inductive families
• Locally cartesian closed categories and type theory
• Polynomial functors and polynomial monads
• Programming in Ωmega
• Purely Functional Data Structures
• Refining inductive types
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Secure distributed programming with value-dependent types
• Stratified type inference for generalized algebraic data types
• The Category-Theoretic Solution of Recursive Domain Equations
• The Zipper
• Transporting functions across ornaments
• Types for Proofs and Programs

Cited in

(6)

• A Categorical Treatment of Ornaments
• Transporting functions across ornaments
• scientific article; zbMATH DE number 490790 (Why is no real title available?)
• Ornaments for Proof Reuse in Coq
• Transporting functions across ornaments
• Programming with ornaments

Describes a project that uses

Uses Software

• Nuprl
• Irdis
• Idris
• F*

This page was built for publication: The essence of ornaments

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