research
∙
06/08/2023
Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts
Progress has recently been made on specifying instruction set architectu...
share
research
∙
07/02/2022
Sikkel: Multimode Simple Type Theory as an Agda Library
Many variants of type theory extend a basic theory with additional primi...
research
∙
10/21/2020
On the Semantic Expressiveness of Recursive Types
Recursive types extend the simply-typed lambda calculus (STLC) with the ...
research
∙
10/15/2020
Abstract Congruence Criteria for Weak Bisimilarity
We introduce three general compositionality criteria over operational se...
research
∙
08/19/2020
Transpension: The Right Adjoint to the Pi-type
Presheaf models of dependent type theory have been successfully applied ...
research
∙
06/02/2020
Uninitialized Capabilities
This technical report describes a new extension to capability machines. ...
research
∙
05/12/2020
CapablePtrs: Securely Compiling Partial Programs using the Pointers-as-Capabilities Principle
Capability machines such as CHERI provide memory capabilities that can b...
research
∙
04/07/2020
A categorical approach to secure compilation
We introduce a novel approach to secure compilation based on maps of dis...
research
∙
02/14/2020
Gavial: Programming the web with multi-tier FRP
Developing web applications requires dealing with their distributed natu...
research
∙
02/14/2019
Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management - Technical Appendix Including Proofs and Details
We propose a calling convention for capability machines with local capab...
research
∙
11/07/2018
StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details
We propose and study StkTokens: a new calling convention that provably e...
research
∙
07/30/2018