Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

act: Technical report

Zoe Paraskevopoulou, Anja Petković Komel, Sophie Rain, Lefteris Lazaropoulos, Alexis Terry

Abstract

This technical report contains the formal definitions and metatheory for the act specification and verification language. It documents the syntax, the operational pointer semantics, the type system and the main metatheoretic results (type-safety).

act: Technical report

Abstract

This technical report contains the formal definitions and metatheory for the act specification and verification language. It documents the syntax, the operational pointer semantics, the type system and the main metatheoretic results (type-safety).

Paper Structure

This paper contains 10 sections, 36 theorems, 22 equations.

Table of Contents

  1. Syntax
  2. Pointer Semantics
  3. Value and Environment Typing
  4. Semantic Entailment
  5. Typing
  6. Well-typed State Environment
  7. Environment Well-Foundedness
  8. Pointer Semantics Lemmas
  9. Typing Lemmas
  10. Type Safety

Key Result

Lemma 6.2

Let $\Sigma$ be well-typed and $\Sigma \vdash \mathit{contract} : \Sigma'$. Then $\Sigma'$ is well-typed. $\blacktriangleleft$$\blacktriangleleft$

Theorems & Definitions (37)

  • Definition 6.1: Well-typed $\Sigma$
  • Lemma 6.2: Extending $\Sigma$ Preserves Well-Typedness
  • Corollary 6.3
  • Theorem 7.1: Well-typed state is well-founded
  • Corollary 7.2: Well-typed state is well-founded
  • Lemma 8.1: Uniqueness of Contract Value Typing
  • Lemma 8.2: Determinism of Base- and Mapping Expression Evaluation
  • Lemma 8.3: Determinism of Reference Evaluation
  • Lemma 8.4: Determinism of Value Insertion
  • Lemma 8.5: Determinism of Slot Expression Evaluation
  • ...and 27 more