During the poster session in ICFP'12 several people asked me about whether further information is available. So, here I posted a PDF of my poster and a draft paper submitted to a conference (now accepted and published in TLCA'13

Poster in ACM SRC hosted by ICFP 2012

SystemFiPosterICFP12ACMSRC.pdf

Draft of our TLCA'13 paper

available online at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.306.3555

BibTeX for citation:

@incollection{
year={2013},
isbn={978-3-642-38945-0},
booktitle={Typed Lambda Calculi and Applications},
volume={7941},
series={Lecture Notes in Computer Science},
editor={Hasegawa, Masahito},
doi={10.1007/978-3-642-38946-7_4},
title={System Fi: a higher-order-polymorphic lambda calculus with erasable term indices},
url={http://dx.doi.org/10.1007/978-3-642-38946-7_4},
publisher={Springer Berlin Heidelberg},
keywords={term-indexed data types; generalized algebraic data types;
 higher-order polymorphism; type-constructor polymorphism;
 higher- kinded types; impredicative encoding;
 strong normalization; logical consistency},
author={Ahn, KiYung and Sheard, Tim and Fiore, Marcelo and Pitts, Andrew M.},
pages={15-30},
}

Presentation material for selected posters

http://prezi.com/t7zrjbfnjx8q/system-fi/

Software

I also have a reference implementation of a Church-style Fi with both beta-conversion and eta-conversion (doesn’t have a parser though, just Haskell syntax tree, normalizer, and type checker)

http://code.google.com/p/trellys/source/browse/trunk/lib/unbound-example/