Gregory Malecha
Gregory Malecha
BedRock Systems, Inc
Verified email at - Homepage
Cited by
Cited by
Toward a verified relational database management system
G Malecha, G Morrisett, A Shinnar, R Wisnesky
ACM SIGPLAN Notices 45 (1), 237-248, 2010
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
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
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
Trace-based verification of imperative programs with I/O
G Malecha, G Morrisett, R Wisnesky
Journal of Symbolic Computation 46 (2), 95-118, 2011
Automated Software Winnowing
G Malecha, A Gehani, N Shankar
Hardware support for safety interlocks and introspection
U Dhawan, A Kwon, E Kadric, C Hritcu, BC Pierce, JM Smith, A DeHon, ...
Draft, July, 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
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
Compositional Computational Reflection
G Malecha, A Chlipala, T Braibant
Interactive Theorem Proving, 0
Formal verification of stability properties of cyber-physical systems
M Chan, D Ricketts, S Lerner, G Malecha
Proc. CoqPL’16, 2016
Extensible and Efficient Automation Through Reflective Tactics
G Malecha, J Bengtson
European Symposium on Programming Languages, 532-559, 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
Extensible Proof Engineering in Intensional Type Theory
G Malecha
Harvard University, 2015
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
Interaction trees
L Xia, Y Zakowski, P He, CK Hur, G Malecha, BC Pierce, S Zdancewic
Proceedings of the ACM on Programming Languages 4, 2020
Mechanized verification with sharing
G Malecha, G Morrisett
International Colloquium on Theoretical Aspects of Computing, 245-259, 2010
Maximum Entropy Part-of-Speech Tagging in NLTK
G Malecha, I Smith
unpublished course-related report, 2010
Certified web services in Ynot
R Wisnesky, GM Malecha, JG Morrisett
Proceedings, 5th International Workshop on Automated Specification and …, 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
The system can't perform the operation now. Try again later.
Articles 1–20