Dominique Devriese

92 papers A* 6A 14B 5C 4Journal 43Unranked 19

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Formalizing the RISC-V Hypervisor Extension in Sail. EuroSec Lowie Deferme, Danny Hughes, Dominique Devriese
2026	J	`jnl`	SoK: Robust properties, robust abstractions and back-translations. J. Comput. Secur. Emiel Lanckriet, Frank Piessens, Dominique Devriese
2025	J	`jnl`	BiSikkel: A Multimode Logical Framework in Agda. Proc. ACM Program. Lang. Joris Ceulemans, Andreas Nuyts, Dominique Devriese
2025	J	`jnl`	Nominal Type Theory by Nullary Internal Parametricity. CoRR Antoine Van Muylder, Andreas Nuyts, Dominique Devriese
2025	J	`jnl`	Towards Computational UIP in Cubical Agda. CoRR Yee-Jian Tan, Andreas Nuyts, Dominique Devriese
2024	J	`jnl`	A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report. CoRR Joris Ceulemans, Andreas Nuyts, Dominique Devriese
2024	J	`jnl`	Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. J. ACM Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal
2024	J	`jnl`	Internal and Observational Parametricity for Cubical Agda. Proc. ACM Program. Lang. Antoine Van Muylder, Andreas Nuyts, Dominique Devriese
2024	J	`jnl`	On the Semantic Expressiveness of Iso- and Equi-Recursive Types. Log. Methods Comput. Sci. Dominique Devriese, Eric Mark Martin, Marco Patrignani
2024	J	`jnl`	Transpension: The Right Adjoint to the Pi-type. Log. Methods Comput. Sci. Andreas Nuyts, Dominique Devriese
2023	A	`conf`	$\pi_{\mathbf{RA}}$: A $\pi\text{-calculus}$ for Verifying Protocols that Use Remote Attestation. CSF Emiel Lanckriet, Matteo Busi, Dominique Devriese
2023	—	`conf`	A Sound and Complete Substitution Algorithm for Multimode Type Theory. TYPES Joris Ceulemans, Andreas Nuyts, Dominique Devriese
2023	A	`conf`	CHERI-TrEE: Flexible enclaves on capability machines. EuroS&P Thomas Van Strydonck, Job Noorman, Jennifer Jackson, Leonardo Alves Dias, Robin Vanderstraeten, David F. Oswald, Frank Piessens, Dominique Devriese
2023	A*	`conf`	Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts. CCS Sander Huyghebaert, Steven Keuchel, Coen De Roover, Dominique Devriese
2023	J	`jnl`	Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts. CoRR Sander Huyghebaert, Steven Keuchel, Coen De Roover, Dominique Devriese
2022	J	`jnl`	Plausible sealing for gradual parametricity. Proc. ACM Program. Lang. Elizabeth Labrada, Matías Toro, Éric Tanter, Dominique Devriese
2022	A	`conf`	Proving full-system security properties under multiple attacker models on capability machines. CSF Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese
2022	J	`jnl`	Purity of an ST monad: full abstraction by semantically typed back-translation. Proc. ACM Program. Lang. Koen Jacobs, Dominique Devriese, Amin Timany
2022	—	`conf`	Sikkel: Multimode Simple Type Theory as an Agda Library. MSFP@ETAPS Joris Ceulemans, Andreas Nuyts, Dominique Devriese
2022	J	`jnl`	Two Parametricities Versus Three Universal Types. ACM Trans. Program. Lang. Syst. Dominique Devriese, Marco Patrignani, Frank Piessens
2022	J	`jnl`	Verified symbolic execution with Kripke specification monads (and no meta-programming). Proc. ACM Program. Lang. Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov, Dominique Devriese
2021	B	`conf`	Abstract Congruence Criteria for Weak Bisimilarity. MFCS Stelios Tsampas, Christian Williams, Andreas Nuyts, Dominique Devriese, Frank Piessens
2021	—	`conf`	Borrowed Capabilities: Flexibly Enforcing Revocation on a Capability Architecture. EuroS&P Workshops Thijs Vercammen, Thomas Van Strydonck, Dominique Devriese
2021	A	`conf`	CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle. CSF Akram El-Korashy, Stelios Tsampas, Marco Patrignani, Dominique Devriese, Deepak Garg, Frank Piessens
2021	J	`jnl`	Efficient and provable local capability revocation using uninitialized capabilities. Proc. ACM Program. Lang. Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal
2021	J	`jnl`	Fully abstract from static to gradual. Proc. ACM Program. Lang. Koen Jacobs, Amin Timany, Dominique Devriese
2021	J	`jnl`	Linear capabilities for fully abstract compilation of separation-logic-verified code. J. Funct. Program. Thomas Van Strydonck, Frank Piessens, Dominique Devriese
2021	J	`jnl`	On the semantic expressiveness of recursive types. Proc. ACM Program. Lang. Marco Patrignani, Eric Mark Martin, Dominique Devriese
2021	J	`jnl`	StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities. J. Funct. Program. Lau Skorstengaard, Dominique Devriese, Lars Birkedal
2020	—	`conf`	A Categorical Approach to Secure Compilation. CMCS Stelios Tsampas, Andreas Nuyts, Dominique Devriese, Frank Piessens
2020	J	`jnl`	A categorical approach to secure compilation. CoRR Stelios Tsampas, Andreas Nuyts, Dominique Devriese, Frank Piessens
2020	J	`jnl`	Abstract Congruence Criteria for Weak Bisimilarity. CoRR Stelios Tsampas, Christian Williams, Dominique Devriese, Frank Piessens
2020	J	`jnl`	CapablePtrs: Securely Compiling Partial Programs using the Pointers-as-Capabilities Principle. CoRR Akram El-Korashy, Stelios Tsampas, Marco Patrignani, Dominique Devriese, Deepak Garg, Frank Piessens
2020	J	`jnl`	Gavial: Programming the web with multi-tier FRP. CoRR Bob Reynders, Frank Piessens, Dominique Devriese
2020	J	`jnl`	Gavial: Programming the web with multi-tier FRP. Art Sci. Eng. Program. Bob Reynders, Frank Piessens, Dominique Devriese
2020	J	`jnl`	Leibniz equality is isomorphic to Martin-Löf identity, parametrically. J. Funct. Program. Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, Philip Wadler
2020	J	`jnl`	On the Semantic Expressiveness of Recursive Types. CoRR Marco Patrignani, Eric Mark Martin, Dominique Devriese
2020	J	`jnl`	Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. ACM Trans. Program. Lang. Syst. Lau Skorstengaard, Dominique Devriese, Lars Birkedal
2020	J	`jnl`	Transpension: The Right Adjoint to the Pi-type. CoRR Andreas Nuyts, Dominique Devriese
2020	J	`jnl`	Uninitialized Capabilities. CoRR Sander Huyghebaert, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese
2019	—	`conf`	How to do proofs: practically proving properties about effectful programs' results (functional pearl). TyDe@ICFP Koen Jacobs, Andreas Nuyts, Dominique Devriese
2019	J	`jnl`	Linear capabilities for fully abstract compilation of separation-logic-verified code. Proc. ACM Program. Lang. Thomas Van Strydonck, Frank Piessens, Dominique Devriese
2019	—	`conf`	Modular effects in Haskell through effect polymorphism and explicit dictionary applications: a new approach and the μVeriFast verifier as a case study. Haskell@ICFP Dominique Devriese
2019	J	`jnl`	Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management - Technical Appendix Including Proofs and Details. CoRR Lau Skorstengaard, Dominique Devriese, Lars Birkedal
2019	J	`jnl`	StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities. Proc. ACM Program. Lang. Lau Skorstengaard, Dominique Devriese, Lars Birkedal
2019	A	`conf`	Temporal Safety for Stack Allocated Memory on Capability Machines. CSF Stelios Tsampas, Dominique Devriese, Frank Piessens
2018	J	`jnl`	Coherent Explicit Dictionary Application for Haskell: Formalisation and Coherence Proof. CoRR Thomas Winant, Dominique Devriese
2018	—	`conf`	Coherent explicit dictionary application for Haskell. Haskell@ICFP Thomas Winant, Dominique Devriese
2018	A*	`conf`	Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory. LICS Andreas Nuyts, Dominique Devriese
2018	J	`jnl`	Parametricity versus the universal type. Proc. ACM Program. Lang. Dominique Devriese, Marco Patrignani, Frank Piessens
2018	J	`jnl`	Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory. J. Funct. Program. Jesper Cockx, Dominique Devriese
2018	A	`conf`	Reasoning About a Machine with Local Capabilities - Provably Safe Stack and Return Pointer Management. ESOP Lau Skorstengaard, Dominique Devriese, Lars Birkedal
2018	—	`conf`	Scalagna 0.1: towards multi-tier programming with Scala and Scala.js. Programming Bob Reynders, Michael Greefs, Dominique Devriese, Frank Piessens
2018	J	`jnl`	StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details. CoRR Lau Skorstengaard, Dominique Devriese, Lars Birkedal
2017	B	`conf`	Efficient Functional Reactive Programming Through Incremental Behaviors. APLAS Bob Reynders, Dominique Devriese
2017	—	`conf`	Elmsvuur: A Multi-tier Version of Elm and its Time-Traveling Debugger. TFP Jeff Horemans, Bob Reynders, Dominique Devriese, Frank Piessens
2017	—	`conf`	Experience Report: Functional Reactive Programming and the DOM. Programming Bob Reynders, Dominique Devriese, Frank Piessens
2017	C	`conf`	Expressive and strongly type-safe code generation. PPDP Thomas Winant, Jesper Cockx, Dominique Devriese
2017	—	`conf`	FRP IoT modules as a Scala DSL. REBLS@SPLASH Ben Calus, Bob Reynders, Dominique Devriese, Job Noorman, Frank Piessens
2017	B	`conf`	Lifting proof-relevant unification to higher dimensions. CPP Jesper Cockx, Dominique Devriese
2017	J	`jnl`	Modular, Fully-abstract Compilation by Approximate Back-translation. CoRR Dominique Devriese, Marco Patrignani, Frank Piessens, Steven Keuchel
2017	J	`jnl`	Modular, Fully-abstract Compilation by Approximate Back-translation. Log. Methods Comput. Sci. Dominique Devriese, Marco Patrignani, Frank Piessens, Steven Keuchel
2017	J	`jnl`	Parametric quantifiers for dependent type theory. Proc. ACM Program. Lang. Andreas Nuyts, Andrea Vezzosi, Dominique Devriese
2016	J	`jnl`	Eliminating dependent pattern matching without K. J. Funct. Program. Jesper Cockx, Dominique Devriese, Frank Piessens
2016	A*	`conf`	Fully-abstract compilation by approximate back-translation. POPL Dominique Devriese, Marco Patrignani, Frank Piessens
2016	J	`jnl`	On Modular and Fully-Abstract Compilation - Technical Appendix. CoRR Marco Patrignani, Dominique Devriese, Frank Piessens
2016	A	`conf`	On Modular and Fully-Abstract Compilation. CSF Marco Patrignani, Dominique Devriese, Frank Piessens
2016	A	`conf`	Reasoning about Object Capabilities with Logical Relations and Effect Parametricity. EuroS&P Dominique Devriese, Lars Birkedal, Frank Piessens
2016	—	`conf`	Security Guarantees for the Execution Infrastructure of Software Applications. SecDev Frank Piessens, Dominique Devriese, Jan Tobias Mühlberg, Raoul Strackx
2016	A	`conf`	Unifiers as equivalences: proof-relevant unification of dependently typed data. ICFP Jesper Cockx, Dominique Devriese, Frank Piessens
2015	B	`conf`	Generating safe boundary APIs between typed EDSLs and their environments. GPCE Bob Reynders, Dominique Devriese, Frank Piessens
2014	—	`—`	Functional Techniques for Representing and Specifying Software (Functionele technieken voor het voorstellen en specifiëren van software). Dominique Devriese
2014	—	`conf`	Multi-Tier Functional Reactive Programming for the Web. Onward! Bob Reynders, Dominique Devriese, Frank Piessens
2014	A	`conf`	Overlapping and Order-Independent Patterns - Definitional Equality for All. ESOP Jesper Cockx, Frank Piessens, Dominique Devriese
2014	C	`conf`	Partial Type Signatures for Haskell. PADL Thomas Winant, Dominique Devriese, Frank Piessens, Tom Schrijvers
2014	A	`conf`	Pattern matching without K. ICFP Jesper Cockx, Dominique Devriese, Frank Piessens
2014	J	`jnl`	Secure multi-execution of web scripts: Theory and practice. J. Comput. Secur. Willem De Groef, Dominique Devriese, Nick Nikiforakis, Frank Piessens
2014	A	`conf`	Stateful Declassification Policies for Event-Driven Programs. CSF Mathy Vanhoef, Willem De Groef, Dominique Devriese, Frank Piessens, Tamara Rezk
2013	C	`conf`	Fixing idioms: a recursion primitive for applicative DSLs. PEPM Dominique Devriese, Ilya Sergey, Dave Clarke, Frank Piessens
2013	—	`conf`	Information Flow Control for Web Scripts. FOSAD Willem De Groef, Dominique Devriese, Mathy Vanhoef, Frank Piessens
2013	A*	`conf`	Monadic abstract interpreters. PLDI Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens
2013	A	`conf`	Typed syntactic meta-programming. ICFP Dominique Devriese, Frank Piessens
2012	J	`jnl`	Finally tagless observable recursion for an abstract grammar model. J. Funct. Program. Dominique Devriese, Frank Piessens
2012	A*	`conf`	FlowFox: a web browser with flexible and precise information flow control. CCS Willem De Groef, Dominique Devriese, Nick Nikiforakis, Frank Piessens
2012	—	`conf`	PESAP: A Privacy Enhanced Social Application Platform. SocialCom/PASSAT Tom Reynaert, Willem De Groef, Dominique Devriese, Lieven Desmet, Frank Piessens
2012	—	`conf`	Secure Multi-Execution through Static Program Transformation. FMOODS/FORTE Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas
2011	—	`conf`	Better Security and Privacy for Web Browsers: A Survey of Techniques, and a New Implementation. Formal Aspects in Security and Trust Willem De Groef, Dominique Devriese, Frank Piessens
2011	C	`conf`	Explicitly Recursive Grammar Combinators - A Better Model for Shallow Parser DSLs. PADL Dominique Devriese, Frank Piessens
2011	—	`conf`	Information flow enforcement in monadic libraries. TLDI Dominique Devriese, Frank Piessens
2011	A	`conf`	On the bright side of type classes: instance arguments in Agda. ICFP Dominique Devriese, Frank Piessens
2011	B	`conf`	Reactive non-interference for a browser model. NSS Nataliia Bielova, Dominique Devriese, Fabio Massacci, Frank Piessens
2010	A*	`conf`	Noninterference through Secure Multi-execution. IEEE Symposium on Security and Privacy Dominique Devriese, Frank Piessens