Scrap your type applications

Jay, B; Peyton Jones, S

Scrap your type applications

Jay, B

Peyton Jones, S

Permalink

Publication Type:: Conference Proceeding
Citation:: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2008, 5133 LNCS pp. 2 - 27
Issue Date:: 2008-08-13

Closed Access

	Filename	Description	Size
	2008001768OK.pdf		419.28 kB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Closed Access

This item is closed access and not available.

Full metadata record

Field	Value	Language
dc.contributor.author	Jay, B https://orcid.org/0000-0001-8654-4305	en_US
dc.contributor.author	Peyton Jones, S	en_US
dc.date.issued	2008-08-13	en_US
dc.identifier.citation	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2008, 5133 LNCS pp. 2 - 27	en_US
dc.identifier.isbn	3540705937	en_US
dc.identifier.isbn	9783540705932	en_US
dc.identifier.issn	0302-9743	en_US
dc.identifier.uri	http://hdl.handle.net/10453/10839
dc.description.abstract	System F is ubiquitous in logic, theorem proving, language meta-theory, compiler intermediate languages, and elsewhere. Along with its type abstractions come type applications, but these often appear redundant. This redundancy is both distracting and costly for type-directed compilers. We introduce System IF, for implicit System F, in which many type applications can be made implicit. It supports decidable type checking and strong normalisation. Experiments with Haskell suggest that it could be used to reduce the amount of intermediate code in compilers that employ System F. System IF constitutes a first foray into a new area in the design space of typed lambda calculi, that is interesting in its own right and may prove useful in practice. © 2008 Springer-Verlag.	en_US
dc.relation.ispartof	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)	en_US
dc.relation.isbasedon	10.1007/978-3-540-70594-9_2	en_US
dc.subject.classification	Artificial Intelligence & Image Processing	en_US
dc.title	Scrap your type applications	en_US
dc.type	Conference Proceeding
utslib.citation.volume	5133 LNCS	en_US
utslib.for	080203 Computational Logic and Formal Languages	en_US
utslib.for	080308 Programming Languages	en_US
dc.location.activity	Marseille, France	en_US
dc.location.activity	Marseille, FRANCE
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology/School of Computer Science
pubs.organisational-group	/University of Technology Sydney/Strength - CAI - Centre for Artificial Intelligence
utslib.copyright.status	closed_access
pubs.publication-status	Published	en_US
pubs.volume	5133 LNCS	en_US

Abstract:

System F is ubiquitous in logic, theorem proving, language meta-theory, compiler intermediate languages, and elsewhere. Along with its type abstractions come type applications, but these often appear redundant. This redundancy is both distracting and costly for type-directed compilers. We introduce System IF, for implicit System F, in which many type applications can be made implicit. It supports decidable type checking and strong normalisation. Experiments with Haskell suggest that it could be used to reduce the amount of intermediate code in compilers that employ System F. System IF constitutes a first foray into a new area in the design space of typed lambda calculi, that is interesting in its own right and may prove useful in practice. © 2008 Springer-Verlag.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/10839