Zachary Tatlock

Orcid: 0000-0002-4731-0124

According to our database1, Zachary Tatlock authored at least 69 papers between 2008 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Application-level Validation of Accelerator Designs Using a Formal Software/Hardware Interface.
ACM Trans. Design Autom. Electr. Syst., March, 2024

There and Back Again: A Netlist's Tale with Much Egraphin'.
CoRR, 2024

Magic Markup: Maintaining Document-External Markup with an LLM.
Proceedings of the Companion Proceedings of the 8th International Conference on the Art, 2024

FPGA Technology Mapping Using Sketch-Guided Program Synthesis.
Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2024

2023
Equality Saturation Theory Exploration à la Carte.
Proc. ACM Program. Lang., October, 2023

babble: Learning Better Abstractions with E-Graphs and Anti-unification.
Proc. ACM Program. Lang., January, 2023

Better Together: Unifying Datalog and Equality Saturation.
Proc. ACM Program. Lang., 2023

Generate Compilers from Hardware Models!
CoRR, 2023

Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting.
Proceedings of the 36th Annual ACM Symposium on User Interface Software and Technology, 2023

Exploring Self-Embedded Knitting Programs with Twine.
Proceedings of the 11th ACM SIGPLAN International Workshop on Functional Art, 2023

2022
Co-Optimization of Design and Fabrication Plans for Carpentry.
ACM Trans. Graph., 2022

Relational e-matching.
Proc. ACM Program. Lang., 2022

Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact).
Dagstuhl Artifacts Ser., 2022

Specialized Accelerators and Compiler Flows: Replacing Accelerator APIs with a Formal Software/Hardware Interface.
CoRR, 2022

Small Proofs from Congruence Closure.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Verified Compilation and Optimization of Floating-Point Programs in CakeML.
Proceedings of the 36th European Conference on Object-Oriented Programming, 2022

2021
egg: Fast and extensible equality saturation.
Proc. ACM Program. Lang., 2021

Rewrite rule inference using equality saturation.
Proc. ACM Program. Lang., 2021

Co-Optimization of Design and Fabrication Plans for Carpentry: Supplemental Material.
CoRR, 2021

Pure tensor program rewriting via access patterns (representation pearl).
Proceedings of the MAPS@PLDI 2021: Proceedings of the 5th ACM SIGPLAN International Symposium on Machine Programming, 2021

Nimble: Efficiently Compiling Dynamic Neural Networks for Model Inference.
Proceedings of the Fourth Conference on Machine Learning and Systems, 2021

Dynamic Tensor Rematerialization.
Proceedings of the 9th International Conference on Learning Representations, 2021

Guarding Numerics Amidst Rising Heterogeneity.
Proceedings of the 5th IEEE/ACM International Workshop on Software Correctness for HPC Applications, 2021

Combining Precision Tuning and Rewriting.
Proceedings of the 28th IEEE Symposium on Computer Arithmetic, 2021

2020
egg: Easy, Efficient, and Extensible E-graphs.
CoRR, 2020

Enumerating Hardware-Software Splits with Program Rewriting.
CoRR, 2020

Towards Numerical Assistants - Trust, Measurement, Community, and Generality for the Numerical Workbench.
Proceedings of the Software Verification - 12th International Conference, 2020

Synthesizing structured CAD models with equality saturation and inverse transformations.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

2019
Carpentry compiler.
ACM Trans. Graph., 2019

Modular verification of web page layout.
Proc. ACM Program. Lang., 2019

QED at Large: A Survey of Engineering of Formally Verified Software.
Found. Trends Program. Lang., 2019

Using E-Graphs for CAD Parameter Inference.
CoRR, 2019

Relay: A High-Level IR for Deep Learning.
CoRR, 2019

Theia: automatically generating correct program state visualizations.
Proceedings of the SPLASH-E '19, 2019

Toward Multi-Precision, Multi-Format Numerics.
Proceedings of the 2019 IEEE/ACM 3rd International Workshop on Software Correctness for HPC Applications (Correctness), 2019

Teaching Rigorous Distributed Systems With Efficient Model Checking.
Proceedings of the Fourteenth EuroSys Conference 2019, Dresden, Germany, March 25-28, 2019, 2019

Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018
Programming and proving with distributed protocols.
Proc. ACM Program. Lang., 2018

Functional programming for compiling and decompiling computer-aided design.
Proc. ACM Program. Lang., 2018

A Graphical Interactive Debugger for Distributed Systems.
CoRR, 2018

Finding root causes of floating point error.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Relay: a new IR for machine learning frameworks.
Proceedings of the 2nd ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, 2018

Verifying that web pages have accessible layout.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper).
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Combining Tools for Optimization and Analysis of Floating-Point Computations.
Proceedings of the Formal Methods - 22nd International Symposium, 2018

Œuf: minimizing the Coq extraction TCB.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017
SpaceSearch: a library for building and verifying solver-aided tools.
Proc. ACM Program. Lang., 2017

Finding Root Causes of Floating Point Error with Herbgrind.
CoRR, 2017

Programming Language Abstractions for Modularly Verified Distributed Systems.
Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

Programming Language Tools and Techniques for 3D Printing.
Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

2016
Verified peephole optimizations for CompCert.
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

Scalable verification of border gateway protocol configurations with an SMT solver.
Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 2016

Planning for change in a formal verification of the raft consensus protocol.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Toward a Standard Benchmark Format and Suite for Floating-Point Analysis.
Proceedings of the Numerical Software Verification - 9th International Workshop, 2016

2015
Toward a Dependability Case Language and Workflow for a Radiation Therapy System.
Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Verdi: a framework for implementing and formally verifying distributed systems.
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Automatically improving accuracy for floating point expressions.
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

RoboFlow: A flow-based visual programming language for mobile manipulation tasks.
Proceedings of the IEEE International Conference on Robotics and Automation, 2015

Visual Robot Programming for Generalizable Mobile Manipulation Tasks.
Proceedings of the Tenth Annual ACM/IEEE International Conference on Human-Robot Interaction, 2015

2014
Reducing the Costs of Proof Assistant Based Formal Verification or : Conviction without the Burden of Proof.
PhD thesis, 2014

Automating formal proofs for reactive systems.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

Jitk: A Trustworthy In-Kernel Interpreter Infrastructure.
Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, 2014

SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks.
Proceedings of the 21st Annual Network and Distributed System Security Symposium, 2014

2012
Establishing Browser Security Guarantees through Formal Shim Verification.
Proceedings of the 21th USENIX Security Symposium, Bellevue, WA, USA, August 8-10, 2012, 2012

2011
Equality Saturation: A New Approach to Optimization
Log. Methods Comput. Sci., 2011

2010
Bringing extensibility to verified compilers.
Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010

2009
Proving optimizations correct using parameterized program equivalence.
Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

2008
Deep typechecking and refactoring.
Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2008


  Loading...