The essence of ornaments

DOI10.1017/S0956796816000356zbMath1418.68032OpenAlexW2181666843MaRDI QIDQ5372005

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

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

Related Items

Ornaments for Proof Reuse in Coq

Uses Software

• Nuprl
• Irdis
• Idris
• F*

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Inductive families
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Refining Inductive Types
• Complete and decidable type inference for GADTs
• Locally cartesian closed categories and type theory
• Programming in Ωmega
• A UNIVERSE OF STRICTLY POSITIVE FAMILIES
• The Category-Theoretic Solution of Recursive Domain Equations
• The Zipper
• Purely Functional Data Structures
• Polynomial functors and polynomial monads
• A set constructor for inductive sets in Martin-Löf's type theory
• Transporting functions across ornaments
• Secure distributed programming with value-dependent types
• A Categorical Treatment of Ornaments
• Stratified type inference for generalized algebraic data types
• Indexed containers
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Types for Proofs and Programs