Foundations for structured programming with GADTs

DOI10.1145/1328438.1328475MaRDI QIDQ3189848zbMATH OpenOpenAlexFDO

Authors Patricia Johann, Neil Ghani

Publication date 12 September 2014

Published in Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://strathprints.strath.ac.uk/33726/

zbMATH Keywords

GADTsinitial algebra semanticsprogram fusion

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65)

Recommendations

• Initial Algebra Semantics Is Enough!
• A principled approach to programming with nested types in Haskell
• Ghostbuster: a tool for simplifying and converting GADTs
• Dualizing generalized algebraic data types by matrix transposition
• A lean specification for gadts: System F with first-class equality proofs

Cited in

(19)

• Shortcut fusion rules for the derivation of circular and higher-order programs
• Parametricity for primitive nested types
• Dualizing generalized algebraic data types by matrix transposition
• Higher-order algebras and coalgebras from parameterized endofunctors
• Dynamic optimization for functional reactive programming using generalized algebraic data types
• Ghostbuster: a tool for simplifying and converting GADTs
• A Framework for Extended Algebraic Data Types
• Parametricity, type equality, and higher-order polymorphism
• Initial Algebra Semantics for Cyclic Sharing Structures
• Parametricity for nested types and GADTs
• Functional semantics
• Fantastic morphisms and where to find them. A guide to recursion schemes
• Structured handling of scoped effects
• Characterizing functions mappable over GADTs
• A lean specification for gadts: System F with first-class equality proofs
• GADTs, functoriality, parametricity: pick two
• GADTs are not (even partial) functors
• Transposing G to \(\text{C}^{\sharp}\): expressivity of generalized algebraic data types in an object-oriented language
• A principled approach to programming with nested types in Haskell

This page was built for publication: Foundations for structured programming with GADTs

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