The essence of ornaments
From MaRDI portal
Publication:5372005
DOI10.1017/S0956796816000356zbMath1418.68032OpenAlexW2181666843MaRDI QIDQ5372005
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
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
Uses Software
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