23 citations · 38 across the 12 of their papers we have counts for
16 papers
SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)
Shixin Song, Davide Davoli, Elias Storme +4
Capability-based architectures such as CHERI provide strong support for the architectural isolation of software components. To additionally protect against microarchitectural leaka…
Nominal Type Theory by Nullary Internal Parametricity
Antoine Van Muylder, Andreas Nuyts, Dominique Devriese
There are many ways to represent the syntax of a language with binders. In particular, nominal frameworks are metalanguages that feature (among others) name abstraction types, whic…
Towards Computational UIP in Cubical Agda
Yee-Jian Tan, Andreas Nuyts, Dominique Devriese
Some advantages of Cubical Type Theory, as implemented by Cubical Agda, over intensional Martin-Löf Type Theory include Quotient Inductive Types (QITs), which exist as instances of…
A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report
Joris Ceulemans, Andreas Nuyts, Dominique Devriese
This is the technical report accompanying the paper "A Sound and Complete Substitution Algorithm for Multimode Type Theory" [Ceulemans, Nuyts and Devriese, 2024]. It contains a ful…
Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts
Sander Huyghebaert, Steven Keuchel, Coen De Roover +1
Progress has recently been made on specifying instruction set architectures (ISAs) in executable formalisms rather than through prose. However, to date, those formal specifications…
Sikkel: Multimode Simple Type Theory as an Agda Library
Joris Ceulemans, Andreas Nuyts, Dominique Devriese
Many variants of type theory extend a basic theory with additional primitives or properties like univalence, guarded recursion or parametricity, to enable constructions or proofs t…