| Simple unification-based type inference for GADTs S Peyton Jones, D Vytiniotis, S Weirich, G Washburn ACM SIGPLAN Notices 41 (9), 50-61, 2006 | 459 | 2006 |
| Mechanized metatheory for the masses: The POPLmark challenge B Aydemir, A Bohannon, M Fairbairn, J Foster, B Pierce, P Sewell, ... Theorem Proving in Higher Order Logics, 50-65, 2005 | 442 | 2005 |
| TALx86: A realistic typed assembly language K Crary, N Glew, D Grossman, R Samuels, F Smith, D Walker, S Weirich, ... 1999 ACM SIGPLAN Workshop on Compiler Support for System Software Atlanta …, 1999 | 333 | 1999 |
| Engineering formal metatheory B Aydemir, A Charguéraud, BC Pierce, R Pollack, S Weirich Acm sigplan notices 43 (1), 3-15, 2008 | 316 | 2008 |
| Practical type inference for arbitrary-rank types D Vytiniotis, S Weirich, S Peyton-jones Journal of Functional Programming 17 (1), 1-82, 2007 | 296 | 2007 |
| Giving Haskell a Promotion BA Yorgey, S Weirich, J Cretin, S Peyton Jones, D Vytiniotis TLDI, 11, 2012 | 246 | 2012 |
| Intensional polymorphism in type-erasure semantics K Crary, S Weirich, G Morrisett ACM SIGPLAN Notices 34 (1), 301-312, 1998 | 165 | 1998 |
| Catching bugs in the web of program invariants C Flanagan, M Flatt, S Krishnamurthi, S Weirich, M Felleisen Proceedings of the ACM SIGPLAN 1996 conference on Programming language …, 1996 | 142 | 1996 |
| Reactive noninterference A Bohannon, BC Pierce, V Sjöberg, S Weirich, S Zdancewic Proceedings of the 16th ACM conference on Computer and communications …, 2009 | 132 | 2009 |
| Dependently typed programming with singletons RA Eisenberg, S Weirich ACM SIGPLAN Notices 47 (12), 117-130, 2012 | 128 | 2012 |
| Flexible type analysis K Crary, S Weirich Proceedings of the fourth ACM SIGPLAN international conference on Functional …, 1999 | 125 | 1999 |
| Contracts made manifest M Greenberg, BC Pierce, S Weirich Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2010 | 108 | 2010 |
| Wobbly types: type inference for generalised algebraic data types SP Jones, G Washburn, S Weirich Technical Report MS-CIS-05-26, Univ. of Pennsylvania, 2004 | 105 | 2004 |
| Closed type families with overlapping equations RA Eisenberg, D Vytiniotis, S Peyton Jones, S Weirich ACM SIGPLAN Notices 49 (1), 671-683, 2014 | 102 | 2014 |
| Combining proofs and programs in a dependently typed language C Casinghino, V Sjöberg, S Weirich ACM SIGPLAN Notices 49 (1), 33-45, 2014 | 87 | 2014 |
| Boxy types: inference for higher-rank types and impredicativity D Vytiniotis, S Weirich, S Peyton Jones Proceedings of the eleventh ACM SIGPLAN international conference on …, 2006 | 85 | 2006 |
| Total haskell is reasonable coq A Spector-Zabusky, J Breitner, C Rizkallah, S Weirich Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018 | 84 | 2018 |
| A specification for dependent types in Haskell S Weirich, A Voizard, PHA de Amorim, RA Eisenberg Proceedings of the ACM on Programming Languages 1 (ICFP), 1-29, 2017 | 83 | 2017 |
| Type-safe cast S Weirich International Conference on Functional Programming (ICFP), 58-67, 2000 | 81* | 2000 |
| Type-safe cast S Weirich ACM SIGPLAN Notices 35 (9), 58-67, 2000 | 81 | 2000 |
Dimitrios VytiniotisDeepMindVerified email at google.com
