The gentle art of levitation
From MaRDI portal
Publication:5176923
DOI10.1145/1863543.1863547zbMath1323.68239MaRDI 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
68N18: Functional programming and lambda calculus
68Q65: Abstract data types; algebraic specification
68P05: Data structures
Related Items
Unnamed Item, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs, POPLMark reloaded: Mechanizing proofs by logical relations, Variations on inductive-recursive definitions, Indexed containers, Programming with ornaments, The calculus of dependent lambda eliminations, From realizability to induction via dependent intersection