The gentle art of levitation
From MaRDI portal
Publication:5176923
DOI10.1145/1863543.1863547zbMath1323.68239OpenAlexW2012619465MaRDI QIDQ5176923
Conor McBride, Pierre-Évariste Dagand, James T. E. Chapman, Peter A. Morris
Publication date: 5 March 2015
Published in: Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1863543.1863547
Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65) Data structures (68P05)
Related Items (8)
From realizability to induction via dependent intersection ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Unnamed Item ⋮ Indexed containers ⋮ Programming with ornaments ⋮ The calculus of dependent lambda eliminations ⋮ Variations on inductive-recursive definitions ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
This page was built for publication: The gentle art of levitation
