| Interaction trees: representing recursive and impure programs in Coq L Xia, Y Zakowski, P He, CK Hur, G Malecha, BC Pierce, S Zdancewic arXiv preprint arXiv:1906.00046, 2019 | 193 | 2019 |
| Toward a verified relational database management system G Malecha, G Morrisett, A Shinnar, R Wisnesky ACM SIGPLAN Notices 45 (1), 237-248, 2010 | 142 | 2010 |
| The MetaCoq Project M Sozeau, A Anand, S Boulier, C Cohen, Y Forster, F Kunze, G Malecha, ... Journal of automated reasoning 64 (5), 947-999, 2020 | 130 | 2020 |
| Effective interactive proofs for higher-order imperative programs A Chlipala, G Malecha, G Morrisett, A Shinnar, R Wisnesky ACM SIGPLAN Notices 44 (9), 79-90, 2009 | 127 | 2009 |
| Automated Software Winnowing G Malecha, A Gehani, N Shankar | 43 | 2015 |
| Trace-based verification of imperative programs with I/O G Malecha, G Morrisett, R Wisnesky Journal of Symbolic Computation 46 (2), 95-118, 2011 | 36 | 2011 |
| Hardware support for safety interlocks and introspection U Dhawan, A Kwon, E Kadric, C Hritcu, BC Pierce, JM Smith, A DeHon, ... Draft, July, 2012 | 30 | 2012 |
| Towards verification of hybrid systems in a foundational proof assistant D Ricketts, G Malecha, MM Alvarez, V Gowda, S Lerner Formal Methods and Models for Codesign (MEMOCODE), 2015 ACM/IEEE …, 2015 | 29 | 2015 |
| Compositional Computational Reflection G Malecha, A Chlipala, T Braibant Interactive Theorem Proving, 0 | 27* | |
| Extensible and Efficient Automation Through Reflective Tactics G Malecha, J Bengtson European Symposium on Programming Languages, 532-559, 2016 | 26 | 2016 |
| Preliminary design of the SAFE platform A DeHon, B Karel, TF Knight Jr, G Malecha, B Montagu, R Morisset, ... Proceedings of the 6th Workshop on Programming Languages and Operating …, 2011 | 26 | 2011 |
| Extensible Proof Engineering in Intensional Type Theory G Malecha Harvard University, 2015 | 23 | 2015 |
| Formal verification of stability properties of cyber-physical systems M Chan, D Ricketts, S Lerner, G Malecha Proc. CoqPL’16, 2016 | 22 | 2016 |
| Towards foundational verification of cyber-physical systems G Malecha, D Ricketts, MM Alvarez, S Lerner Cyber-Physical Systems Workshop (SOSCYPS), Science of Security for, 1-5, 2016 | 19 | 2016 |
| Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee Verilog synthesizability J Gillenwater, G Malecha, C Salama, AY Zhu, W Taha, J Grundy, ... Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and …, 2008 | 17 | 2008 |
| Maximum Entropy Part-of-Speech Tagging in NLTK G Malecha, I Smith unpublished course-related report, 2010 | 15 | 2010 |
| Mechanized verification with sharing G Malecha, G Morrisett International Colloquium on Theoretical Aspects of Computing, 245-259, 2010 | 13 | 2010 |
| Static consistency checking for Verilog wire interconnects: Using dependent types to check the sanity of Verilog descriptions C Salama, G Malecha, W Taha, J Grundy, J O'Leary Proceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and …, 2009 | 13 | 2009 |
| Certified web services in Ynot R Wisnesky, GM Malecha, JG Morrisett Proceedings, 5th International Workshop on Automated Specification and …, 2010 | 12 | 2010 |
| A more precise security type system for dynamic security tests G Malecha, S Chong Proceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and …, 2010 | 8 | 2010 |
Greg MorrisettDean and Professor, Cornell UniversityCorreu electrònic verificat a cornell.edu
