Gregory Malecha

Orcid: 0000-0003-3952-0807

Affiliations:

BedRock Systems, Menlo Park, USA
Harvard University, Cambridge, USA (former)

According to our database¹, Gregory Malecha authored at least 23 papers between 2008 and 2022.

Collaborative distances:

Dijkstra number² of three.
Erdős number³ of four.

Timeline

Legend:

Book

In proceedings

Article

PhD thesis

Dataset

Other

Bibliography

2022

Developing With Formal Methods at BedRock Systems, Inc.

[BibT_eX]

[DOI]

IEEE Secur. Priv., 2022

2021

Formal Methods for the Informal Engineer: Workshop Recommendations.

[BibT_eX]

[DOI]

CoRR, 2021

2020

Interaction trees: representing recursive and impure programs in Coq.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

The MetaCoq Project.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

2019

Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress).

[BibT_eX]

[DOI]

CoRR, 2019

2016

Extensible and Efficient Automation Through Reflective Tactics.

[BibT_eX]

[DOI]

Gregory Malecha

Jesper Bengtson

Proceedings of the Programming Languages and Systems, 2016

Modular deductive verification of sampled-data systems.

[BibT_eX]

[DOI]

Daniel Ricketts

Gregory Malecha

Sorin Lerner

Proceedings of the 2016 International Conference on Embedded Software, 2016

Towards foundational verification of cyber-physical systems.

[BibT_eX]

[DOI]

Proceedings of the 2016 Science of Security for Cyber-Physical Systems Workshop, 2016

2015

Automated software winnowing.

[BibT_eX]

[DOI]

Gregory Malecha

Ashish Gehani

Natarajan Shankar

Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015

Towards verification of hybrid systems in a foundational proof assistant.

[BibT_eX]

[DOI]

Proceedings of the 13. ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2015

Using dependent types and tactics to enable semantic optimization of language-integrated queries.

[BibT_eX]

[DOI]

Gregory Malecha

Ryan Wisnesky

Proceedings of the 15th Symposium on Database Programming Languages, 2015

2014

Compositional Computational Reflection.

[BibT_eX]

[DOI]

Gregory Malecha

Adam Chlipala

Thomas Braibant

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013

MirrorShard: Proof by Computational Reflection with Verified Hints

[BibT_eX]

[DOI]

CoRR, 2013

2012

Hardware Support for Safety Interlocks and Introspection.

[BibT_eX]

[DOI]

Proceedings of the Sixth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, 2012

2011

Static consistency checking for Verilog wire interconnects - Using dependent types to check the sanity of Verilog descriptions.

[BibT_eX]

[DOI]

High. Order Symb. Comput., 2011

Trace-based verification of imperative programs with I/O.

[BibT_eX]

[DOI]

Gregory Malecha

Greg Morrisett

Ryan Wisnesky

J. Symb. Comput., 2011

Preliminary design of the SAFE platform.

[BibT_eX]

[DOI]

Proceedings of the 6th Workshop on Programming Languages and Operating Systems, 2011

2010

Synthesizable High Level Hardware Descriptions.

[BibT_eX]

[DOI]

New Gener. Comput., 2010

Toward a verified relational database management system.

[BibT_eX]

[DOI]

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

A more precise security type system for dynamic security tests.

[BibT_eX]

[DOI]

Gregory Malecha

Stephen Chong

Proceedings of the 2010 Workshop on Programming Languages and Analysis for Security, 2010

Mechanized Verification with Sharing.

[BibT_eX]

[DOI]

J. Gregory Malecha

Greg Morrisett

Proceedings of the Theoretical Aspects of Computing, 2010

2009

Effective interactive proofs for higher-order imperative programs.

[BibT_eX]

[DOI]

Proceedings of the Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, 2009

2008

Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability.

[BibT_eX]

[DOI]

Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, 2008

Gregory Malecha

Timeline

Legend:

Links

Online presence:

On csauthors.net:

Bibliography

Loading...