9 citations · 10 across the 4 of their papers we have counts for
4 papers · 1 filter
Domain Reasoning in TopKAT
Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi
TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the to…
On Pitts' Relational Properties of Domains
Arthur Azevedo de Amorim
Andrew Pitts' framework of relational properties of domains is a powerful method for defining predicates or relations on domains, with applications ranging from reasoning principle…
The Meaning of Memory Safety
Arthur Azevedo de Amorim, Catalin Hritcu, Benjamin C. Pierce
We give a rigorous characterization of what it means for a programming language to be memory safe, capturing the intuition that memory safety supports local reasoning about state.…
Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components
Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim +3
Secure compilation prevents all low-level attacks on compiled code and allows for sound reasoning about security in the source language. In this work we propose a new attacker mode…