Stories by matt_d

Exploiting Microarchitectural Optimizations from Software [pdf]

Making Software Sandboxing Practical Using Language-Based Techniques

TSO and IBM System/370

75 Years of the Microprocessor

Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models

Correctness of C Implementations of Dijkstra’s, Kruskal’s, and Prim’s Algorithms

Sham: A DSL for Fast DSLs

Model Checking C++ Programs

Classical (Co)Recursion: Programming

The Lean 4 Theorem Prover and Programming Language

Native Implementation of Mutable Value Semantics

Programming Languages + Human-Computer Interaction: SPLASH 2020

Accelerator Integration for Open-Source SoC Design [pdf]

The future of programming with certified program synthesis

The Dawn of Formalized Mathematics

Static Integer Types

From Hardware Description Languages to Accelerator Design Languages

The Dawn of Formalized Mathematics

Verifying an HTTP Key-Value Server with Interaction Trees and VST

Threaded Code Generation with a Meta-Tracing JIT Compiler

43
44
45
46
47
48
49
50
51
52