research
∙
11/15/2021
Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda
This document provides a formal proof of Birkhoff's completeness theorem...
share
research
∙
07/29/2021
uiCA: Accurate Throughput Prediction of Basic Blocks on Recent Intel Microarchitectures
Performance models that statically predict the steady-state throughput o...
research
∙
05/28/2020
Flushgeist: Cache Leaks from Beyond the Flush
Flushing the cache, using instructions like clflush and wbinvd, is commo...
research
∙
11/19/2019
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality
In type theory with an impredicative universe of propositions and a proo...
research
∙
11/08/2019
nanoBench: A Low-Overhead Tool for Running Microbenchmarks on x86 Systems
We present nanoBench, a tool for evaluating small microbenchmarks using ...
research
∙
05/07/2019
A Type Theory for Defining Logics and Proofs
We describe a Martin-Löf-style dependent type theory, called Cocon, that...
research
∙
02/16/2019
Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus
We observe that normalization by evaluation for simply-typed lambda-calc...
research
∙
01/10/2019
Cocon: Computation in Contextual Type Theory
We describe a Martin-Löf style dependent type theory, called Cocon, that...
research
∙
10/10/2018