| [1] |
Dimitrios Vytiniotis and Stephanie Weirich.
Type-safe cast does no harm, 2007. [ bib | .pdf ] |
| [2] |
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey
Washburn.
Simple unification-based type inference for GADTs.
In ICFP '06: Proceedings of the Eleventh ACM SIGPLAN
International Conference on Functional Programming, pages 50-61, New York,
NY, USA, 2006. ACM Press. [ bib | .pdf ] |
| [3] |
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones.
Boxy types: inference for higher-rank types and
impredicativity.
In ICFP '06: Proceedings of the Eleventh ACM SIGPLAN
International Conference on Functional Programming, pages 251-262, New
York, NY, USA, 2006. ACM Press. [ bib | .pdf ] |
| [4] |
B. Aydemir, A. Bohannon, M. Fairbairn, J. Foster, B. Pierce, P. Sewell,
D. Vytiniotis, G. Washburn, S. Weirich, and S. Zdancewic.
Mechanized metatheory for the masses: The POPLmark Challenge.
In Proceedings of the Eighteenth International Conference on
Theorem Proving in Higher Order Logics (TPHOLs 2005), 2005. [ bib | http ] |
| [5] |
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark
Shields.
Practical type inference for arbitrary-rank types.
J. Funct. Program., 17(1):1-82, 2007. [ bib | http ] |
| [6] |
Dimitrios Vytiniotis, Geoffrey Washburn, and Stephanie Weirich.
An Open and Shut Typecase.
In The Second ACM SIGPLAN Workshop on Types in Language Design
and Implementation, pages 13-24, Long Beach, California, January 2005. ACM
SIGPLAN. [ bib | .ps ] |
| [7] |
Dimitrios Vytiniotis and Stephanie Weirich.
Free Theorems and Runtime Type Representations.
In M. Fiore and M. Mislove, editors, Proceedings of the 23rd
Annual Conference on Mathematical Foundations of Programming Semantics
(MFPS XXIII), volume 173 of Electronic Notes in Theoretical Computer
Science, pages 357-373, 2007. [ bib | .pdf ] |
| [8] |
Dimitrios Vytiniotis and Stephanie Weirich.
Dependent Types: Easy as Pie.
In Marco T. Morazán and Henrik Nilsson, editors, Draft
Proceedings of the 8th Symposium on Trends in Functional Programming. Dept.
of Math and Computer Science, Seton Hall University, TR-SHU-CS-2007-04-1,
April 2007. [ bib | .pdf ] |
| [9] |
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones.
Practical type inference for arbitrary-rank types, Technical
Appendix.
Technical Report MS-CIS-05-14, University of Pennsylvania, July 2005. [ bib | .pdf ] |
| [10] |
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones.
Boxy type inference for higher-rank types and impredicativity,
Technical Appendix.
Technical Report MS-CIS-05-23, University of Pennsylvania, April
2006. [ bib | .pdf ] |
| [11] |
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones.
Simple unification-based type inference for GADTs, Technical
Appendix.
Technical Report MS-CIS-05-22, University of Pennsylvania, April
2006. [ bib | .pdf ] |
| [12] |
Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn.
An Open and Shut Typecase.
Technical Report MS-CIS-04-26, University of Pennsylvania, April
2004. [ bib | .ps ] |
| [13] |
Nate Foster and Dimitrios Vytiniotis.
A Theory of Featherweight Java in Isabelle/HOL.
In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors,
The Archive of Formal Proofs.
http://afp.sourceforge.net/entries/FeatherweightJava.shtml, March 2006.
Formal proof development. [ bib ] |