Towards an Axiomatic Basis for C++

Gregory Malecha, Abhishek Anand, and Gordon Stewart

Coq Workshop 2020 - 2020

coq c++ program verification separation logic axiomatic semantics

Interaction Trees: Representing Recursive and Impure Programs in Coq

Li-yao Xai, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic

POPL'20 - 2020

coq coinduction denotational semantics

Compositional Non-termination without Fuel

Gregory Malecha

NEPLS'18 - 2018

coq coinduction denotational semantics

Predicate Monads

Edwin Westbrook and Gregory Malecha

CoqPL'17 - 2017

coq monads verification logic

Modular Deductive Verification of Sampled-Data Systems

Daniel Ricketts and Gregory Malecha and Sorin Lerner

EMSOFT'16 - 2016

coq veridrone cyber-physical

Towards Foundational Verification of Cyber-physical Systems

Gregory Malecha, Daniel Ricketts, Mario M. Alvarez, Sorin Lerner

SoSCYPS'16 - 2016

coq veridrone cyber-physical

Formal Verification of Stability Properties in Cyber-physical Systems

Matthew Chan, Daniel Ricketts, Sorin Lerner, Gregory Malecha

CoqPL'16 - 2016

cyber-physical systems veridrone stability

Extensible and Efficient Automation through Reflective Tactics

Gregory Malecha and Jesper Bengtson

ESOP'16 - 2016

coq rtac computation reflection automation

Towards Verification of Hybrid Systems in a Foundational Proof Assistant

Daniel Ricketts, Gregory Malecha, Mario M. Alvarez, Vignesh Gowda and Sorin Lerner

MEMOCODE'15 - 2015

cyber-physical systems verification

Using Dependent Types and Tactics to Enable Semantic Optimization of Language-Integrated Queries

Gregory Malecha and Ryan Wisnesky

DBPL'15 - 2015

coq refinment databases optimization

Extensible Proof Engineering in Intensional Type Theory

Gregory Malecha

PhD Dissertation - 2015

mirror-core rtac coq computational reflection

Rtac: A Fully Reflective Tactic Language

Gregory Malecha and Jesper Bengston

CoqPL'15 - 2015

rtac coq computational reflection automation

Automating Abstract Logics (a.k.a. Implementing Reflective Tactics)

Gregory Malecha, Jesper Bengston, and Adam Chlipala

Coq'14 - 2014

mirror-core coq computational reflection automation talk

Compositional Computational Reflection

Gregory Malecha, Thomas Braibant, and Adam Chlipala

ITP'14 - 2014

mirror-core coq computational reflection automation

MirrorShard: Proof by Computational Reflection with Verified Hints

Gregory Malecha, Adam Chlipala, Thomas Braibant, Patrick Hulin, and Edward Yang

Tech Report - 2013

mirror-shard coq computational reflection automation

Reflecting Modular Automation

Gregory Malecha

Talk @ INRIA - 2013

talk coq mirror-shard computational reflection

Compiling Coq in Coq

Gregory Malecha

Talk @ INRIA - 2013

coq compilation

Building Bedrock: Verifying a Program Verifier

Gregory Malecha, Adam Chlipala, Thomas Braibant, Patrick Hulin, and Edward Yang

Coq'13 - 2012

mirror-shard coq computational reflection automation

Mechanized Verification with Sharing

Gregory Malecha, Greg Morrisett

ICTAC'10 - 2010

coq separation logic ynot

A More Precise Security Type System for Dynamic Security Tests

Gregory Malecha and Stephen Chong

PLAS'10 - 2010

information flow security

Toward a verified relational database management system

Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky

POPL'10 - 2010

ynot coq b+ tree separation logic

Trace-based verification of imperative programs with I/O

Gregory Malecha and Greg Morrisett and Ryan Wisnesky

JSC'11 - 2010

ynot separation logic coq verification

Effective interactive proofs for higher-order imperative programs

Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky

ICFP'09 - 2009

ynot separation logic coq verification