License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2013.20
URN: urn:nbn:de:0030-drops-40506
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4050/
Go to the corresponding LIPIcs Volume Portal

Vytiniotis, Dimitrios ; Peyton Jones, Simon

Evidence Normalization in System FC (Invited Talk)

pdf-format:
3.pdf (0.6 MB)

Abstract

System FC is an explicitly typed language that serves as the target language for Haskell source programs. System FC is based on System F with the addition of erasable but explicit type equality proof witnesses. Equality proof witnesses are generated from type inference performed on source Haskell programs. Such witnesses may be very large objects, which causes performance degradation in later stages of compilation, and makes it hard to debug the results of type inference and subsequent program transformations. In this paper we present an equality proof simplification algorithm, implemented in GHC, which greatly reduces the size of the target System FC programs.

BibTeX - Entry

@InProceedings{vytiniotis_et_al:LIPIcs:2013:4050,
  author =	{Dimitrios Vytiniotis and Simon Peyton Jones},
  title =	{{Evidence Normalization in System FC (Invited Talk)}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{20--38},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{Femke van Raamsdonk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4050},
  URN =		{urn:nbn:de:0030-drops-40506},
  doi =		{10.4230/LIPIcs.RTA.2013.20},
  annote =	{Keywords: Haskell, type functions, system FC}
}

Keywords: Haskell, type functions, system FC
Collection: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Issue Date: 2013
Date of publication: 24.06.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI