System FC with explicit kind equality

DOI10.1145/2500365.2500599MaRDI QIDQ5244807zbMATH OpenOpenAlexFDO

Authors Stephanie Weirich, Justin Hsu, Richard A. Eisenberg

Publication date 30 March 2015

Published in Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://repository.brynmawr.edu/compsci_pubs/9

zbMATH Keywords

dependent typesequalityHaskell

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Evidence normalization in System FC (invited talk)
• Type checking with open type functions
• Adding equations to System F types
• System F in Agda, for fun and profit
• A type-preserving compiler in Haskell

Cited in

(6)

• Evidence normalization in System FC (invited talk)
• Algebraic dynamic programming for multiple context-free grammars
• Unified syntax with iso-types
• A reflection on types
• Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
• \(\eta\)-equivalence in core dependent Haskell

Describes a project that uses

Uses Software

• GHC
• Haskell

This page was built for publication: System FC with explicit kind equality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5244807)