Zobrazeno 1 - 10
of 36
pro vyhledávání: '"Koutavas, Vasileios"'
We present a big-step and small-step operational semantics for Yul -- the intermediate language used by the Solidity compiler to produce EVM bytecode -- in a mathematical notation that is congruous with the literature of programming languages, lends
Externí odkaz:
http://arxiv.org/abs/2407.01365
We propose Pushdown Normal Form (PDNF) Bisimulation to verify contextual equivalence in higher-order functional programming languages with local state. Similar to previous work on Normal Form (NF) bisimulation, PDNF Bisimulation is sound and complete
Externí odkaz:
http://arxiv.org/abs/2311.01325
We present the first fully abstract normal form bisimulation for call-by-value PCF (PCF$_{\textsf{v}}$). Our model is based on a labelled transition system (LTS) that combines elements from applicative bisimulation, environmental bisimulation and gam
Externí odkaz:
http://arxiv.org/abs/2310.01069
Publikováno v:
EPTCS 368, 2022, pp. 60-74
We present an alternative translation from CCS to an extension of CSP based on m-among-n synchronisation (called CSPmn). This translation is correct up to strong bisimulation. Unlike the g-star renaming approach ([4]), this translation is not limited
Externí odkaz:
http://arxiv.org/abs/2209.05232
We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, novel up-to techniques, and lightweigh
Externí odkaz:
http://arxiv.org/abs/2105.02541
Autor:
de Vries, Edsko, Koutavas, Vasileios
We define "Locally Nameless Permutation Types", which fuse permutation types as used in Nominal Isabelle with the locally nameless representation. We show that this combination is particularly useful when formalizing programming languages where bound
Externí odkaz:
http://arxiv.org/abs/1710.08444
Communicating transactions is a form of distributed, non-isolated transactions which provides a simple construct for building concurrent systems. In this paper we develop a logical framework to express properties of the observable behaviour of such s
Externí odkaz:
http://arxiv.org/abs/1703.03256
We study the theory of safety and liveness in a reversible calculus where reductions are totally ordered and rollbacks lead the systems to past states. Similar to previous work on communicating transactions, liveness and safety respectively correspon
Externí odkaz:
http://arxiv.org/abs/1604.05555
We propose a type-based analysis to infer the session protocols of channels in an ML-like concurrent functional language. Combining and extending well-known techniques, we develop a type-checking system that separates the underlying ML type system fr
Externí odkaz:
http://arxiv.org/abs/1510.03929
Autor:
Koutavas, Vasileios.
Publikováno v:
View dissertation online.
Thesis (Ph. D.)--Northeastern University, 2008.
Title from title page (viewed March 24, 2009). College of Computer and Information Science. Includes bibliographical references (p. 163-171).
Title from title page (viewed March 24, 2009). College of Computer and Information Science. Includes bibliographical references (p. 163-171).
Externí odkaz:
http://hdl.handle.net/2047/d10016545
