Skip to main content

Translating Generalized Algebraic Data Types to System F

Sulzmann, Martin and Wang, Meng (2005) Translating Generalized Algebraic Data Types to System F. Technical report. National University of Singapore (Unpublished) (KAR id:47488)

PDF
Language: English
Download (270kB) Preview
[thumbnail of 10.1.1.111.5082.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL
http://citeseerx.ist.psu.edu/viewdoc/download?doi=...

Abstract

Generalized algebraic data types (GADTs) extend ordinary

equality constraints. This is highly useful and allows for novel applications

GADTs we need to enrich the System F style typed intermediate

constraints. We show that GADTs can be translated to a minor extension

F typable proof terms. At run-time proof terms evaluate to the identity.

provide evidence that our approach scales to deal with extensions where

checking of target programs remains as simple as type checking in System

and extensions of it into existing implementations.

Item Type: Monograph (Technical report)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Meng Wang
Date Deposited: 01 Mar 2015 16:55 UTC
Last Modified: 16 Feb 2021 13:23 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/47488 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year