F-ing modules

DOI10.1017/S0956796814000264zbMath1322.68048MaRDI QIDQ4983210

Andreas Rossberg, Claudio V. Russo, Derek R. Dreyer

Publication date: 25 March 2015

Published in: Journal of Functional Programming (Search for Journal in Brave)

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

The Essence of Dependent Object Types ⋮ 1ML with Special Effects ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ The locally nameless representation ⋮ 1ML – Core and modules united ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Mechanizing metatheory without typing contexts

Uses Software

• OCaml

Cites Work

• Unnamed Item
• Unnamed Item
• Bounded existentials and minimal typing
• The undecidability of the second-order unification problem
• A syntactic theory of type generativity and sharing
• A modular module system
• Extensional equivalence and singleton types
• Recursive type generativity
• Acute: High-level programming language design for distributed computation