A lean specification for gadts: System F with first-class equality proofs

DOI10.1007/s10990-011-9065-0zbMath1232.68029OpenAlexW2082517951MaRDI QIDQ656862

Arie Middelkoop, Atze Dijkstra, S. Doaitse Swierstra

Publication date: 13 January 2012

Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10990-011-9065-0

zbMATH Keywords

type systemsystem Fequality proofGADT

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Zipping strategies and attribute grammars ⋮ Transposing G to \(\text{C}^{\sharp}\): expressivity of generalized algebraic data types in an object-oriented language

Uses Software

• Haskell

Cites Work

• Unnamed Item
• Complete and decidable type inference for GADTs
• Typing dynamic typing
• A Framework for Extended Algebraic Data Types
• Libraries for Generic Programming in Haskell
• Efficient self-interpretation in lambda calculus
• Stratified type inference for generalized algebraic data types
• Principal Type Inference for GHC-Style Multi-parameter Type Classes
• Boxy types

This page was built for publication: A lean specification for gadts: System F with first-class equality proofs