Zobrazeno 1 - 10
of 114
pro vyhledávání: '"Devriese, Dominique"'
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 full definition of Well-Scoped Multimode Type Theory (WSMTT) in Section 2
Externí odkaz:
http://arxiv.org/abs/2406.13622
Progress has recently been made on specifying instruction set architectures (ISAs) in executable formalisms rather than through prose. However, to date, those formal specifications are limited to the functional aspects of the ISA and do not cover its
Externí odkaz:
http://arxiv.org/abs/2306.05128
Publikováno v:
EPTCS 360, 2022, pp. 93-112
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 that would be harder or impossible to do in the original theory. Howeve
Externí odkaz:
http://arxiv.org/abs/2207.00843
Recursive types extend the simply-typed lambda calculus (STLC) with the additional expressive power to enable diverging computation and to encode recursive data-types (e.g., lists). Two formulations of recursive types exist: iso-recursive and equi-re
Externí odkaz:
http://arxiv.org/abs/2010.10859
We introduce three general compositionality criteria over operational semantics and prove that, when all three are satisfied together, they guarantee weak bisimulation being a congruence. Our work is founded upon Turi and Plotkin's mathematical opera
Externí odkaz:
http://arxiv.org/abs/2010.07899
Autor:
Nuyts, Andreas, Devriese, Dominique
Publikováno v:
Logical Methods in Computer Science, Volume 20, Issue 2 (June 19, 2024) lmcs:6725
Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable interest in internalizing aspects of these presheaf models, either to mak
Externí odkaz:
http://arxiv.org/abs/2008.08533
This technical report describes a new extension to capability machines. Capability machines are a special type of processors that include better security primitives at the hardware level. In capability machines, every word has an associated tag bit t
Externí odkaz:
http://arxiv.org/abs/2006.01608
Autor:
El-Korashy, Akram, Tsampas, Stelios, Patrignani, Marco, Devriese, Dominique, Garg, Deepak, Piessens, Frank
Capability machines such as CHERI provide memory capabilities that can be used by compilers to provide security benefits for compiled code (e.g., memory safety). The existing C to CHERI compiler, for example, achieves memory safety by following a pri
Externí odkaz:
http://arxiv.org/abs/2005.05944
We introduce a novel approach to secure compilation based on maps of distributive laws. We demonstrate through four examples that the coherence criterion for maps of distributive laws can potentially be a viable alternative for compiler security inst
Externí odkaz:
http://arxiv.org/abs/2004.03557
Publikováno v:
The Art, Science, and Engineering of Programming, 2020, Vol. 4, Issue 3, Article 6
Developing web applications requires dealing with their distributed nature and the natural asynchronicity of user input and network communication. For facilitating this, different researchers have explored the combination of a multi-tier programming
Externí odkaz:
http://arxiv.org/abs/2002.06188