scholarly journals Mechanized Theory of Event Structures: A Case of Parallel Register Machine

2021 ◽  
Vol 33 (3) ◽  
pp. 143-154
Author(s):  
Vladimir Gladstein ◽  
Dmitrii Mikhailovskii ◽  
Evgenii Moiseenko ◽  
Anton Trunov
Keyword(s):  
True Concurrency ◽  
Atomic Actions ◽  
Event Structures ◽  
The Coq Proof Assistant ◽  
Register Machine ◽  
Interleaving Semantics ◽  
Coq Proof Assistant ◽  
Concise Representation ◽  
The Individual ◽  
Semantics Of Concurrency

The true concurrency models, and in particular event structures, have been introduced in the 1980s as an alternative to operational interleaving semantics of concurrency, and nowadays they are regaining popularity. Event structures represent the causal dependency and conflict between the individual atomic actions of the system directly. This property leads to a more compact and concise representation of semantics. In this work-in-progress report, we present a theory of event structures mechanized in the COQ proof assistant and demonstrate how it can be applied to define certified executable semantics of a simple parallel register machine with shared memory.

scholarly journals Homotopy limits in type theory

2015 ◽  
Vol 25 (5) ◽  
pp. 1040-1070 ◽  
Author(s):  
JEREMY AVIGAD ◽  
KRZYSZTOF KAPULKIN ◽  
PETER LEFANU LUMSDAINE
Keyword(s):  
Homotopy Type ◽  
Systematic Study ◽  
Type Theory ◽  
Proof Assistant ◽  
Classical Approach ◽  
Homotopy Type Theory ◽  
The Coq Proof Assistant ◽  
Homotopy Limits ◽  
Coq Proof Assistant

Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.

scholarly journals Residual theory in λ-calculus: a formal development

1994 ◽  
Vol 4 (3) ◽  
pp. 371-394 ◽  
Author(s):  
Gérard Huet
Keyword(s):  
Normal Forms ◽  
Data Types ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant ◽  
Concrete Syntax ◽  
Calculus Of Inductive Constructions ◽  
Recursive Definitions ◽  
Abstract Framework ◽  
Order Predicate Calculus ◽  
Standard Library

AbstractWe present the complete development, in Gallina, of the residual theory of β-reduction in pure λ-calculus. The main result is the Prism Theorem, and its corollary Lévy's Cube Lemma, a strong form of the parallel-moves lemma, itself a key step towards the confluence theorem and its usual corollaries (Church-Rosser, uniqueness of normal forms). Gallina is the specification language of the Coq Proof Assistant (Dowek et al., 1991; Huet 1992b). It is a specific concrete syntax for its abstract framework, the Calculus of Inductive Constructions (Paulin-Mohring, 1993). It may be thought of as a smooth mixture of higher-order predicate calculus with recursive definitions, inductively defined data types and inductive predicate definitions reminiscent of logic programming. The development presented here was fully checked in the current distribution version Coq V5.8. We just state the lemmas in the order in which they are proved, omitting the proof justifications. The full transcript is available as a standard library in the distribution of Coq.

Every bit counts: The binary representation of typed data and programs

2012 ◽  
Vol 22 (4-5) ◽  
pp. 529-573 ◽  
Author(s):  
ANDREW J. KENNEDY ◽  
DIMITRIOS VYTINIOTIS
Keyword(s):  
Binary Data ◽  
General Framework ◽  
Binary Representation ◽  
Proof Assistant ◽  
A Value ◽  
The Coq Proof Assistant ◽  
Binary Encoding ◽  
Coq Proof Assistant ◽  
Definition Of ◽  
Formal Properties

AbstractWe show how the binary encoding and decoding of typed data and typed programs can be understood, programmed and verified with the help of question–answer games. The encoding of a value is determined by the yes/no answers to a sequence of questions about that value; conversely, decoding is the interpretation of binary data as answers to the same question scheme. We introduce a general framework for writing and verifying game-based codecs. We present games in Haskell for structured, recursive, polymorphic and indexed types, building up to a representation of well-typed terms in the simply-typed λ-calculus with polymorphic constants. The framework makes novel use of isomorphisms between types in the definition of games. The definition of isomorphisms together with additional simple properties make it easy to prove that codecs derived from games never encode two distinct values using the same code, never decode two codes to the same value and interpret any bit sequence as a valid code for a value or as a prefix of a valid code. Formal properties of the framework have been proved using the Coq proof assistant.

scholarly journals Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-28
Author(s):  
Adam Chlipala
Keyword(s):  
Order Reduction ◽  
Separation Logic ◽  
Variable Binding ◽  
Type Checking ◽  
Session Types ◽  
The Coq Proof Assistant ◽  
Reduction Program ◽  
Coq Proof Assistant ◽  
Big Ideas ◽  
Concurrent Separation Logic

Rigorous reasoning about programs calls for some amount of bureaucracy in managing details like variable binding, but, in guiding students through big ideas in semantics, we might hope to minimize the overhead. We describe our experiment introducing a range of such ideas, using the Coq proof assistant, without any explicit representation of variables, instead using a higher-order syntax encoding that we dub "mixed embedding": it is neither the fully explicit syntax of deep embeddings nor the syntax-free programming of shallow embeddings. Marquee examples include different takes on concurrency reasoning, including in the traditions of model checking (partial-order reduction), program logics (concurrent separation logic), and type checking (session types) -- all presented without any side conditions on variables.

scholarly journals A formal approach for the verification of the permission-based security model of Android

2018 ◽  
Vol 21 (2) ◽  
Author(s):  
Carlos Luna ◽  
Gustavo Betarte ◽  
Juan Campo ◽  
Camila Sanz ◽  
Maximiliano Cristiá ◽  
...  
Keyword(s):  
Formal Specification ◽  
Control Policy ◽  
Proof Assistant ◽  
Security Model ◽  
Access Control Policy ◽  
Formal Approach ◽  
Fundamental Properties ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant ◽  
Security Properties

This article reports on our experiences in applying formal methods to verify the security mechanisms of Android. We have developed a comprehensive formal specification of Android's permission model, which has been used to state and prove properties that establish expected behavior of the procedures that enforce the defined access control policy. We are also interested in providing guarantees concerning actual implementations of the mechanisms. Therefore we are following a verification approach that combines the use of idealized models, on which fundamental properties are formally verified, with testing of actual implementations using lightweight model-based techniques. We describe the formalized model, present security properties that have been proved using the Coq proof assistant and propose the use of a certified algorithm for performing verification activities such as monitoring of actual implementations of the platform and also as a testing oracle.

scholarly journals Ownership and Immutability in Coq

2021 ◽  
Author(s):  
◽  
Julian Mackay
Keyword(s):  
Programming Languages ◽  
Management System ◽  
Type Systems ◽  
Formal Proof ◽  
Proof Assistant ◽  
Significant Issue ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant

<p>A significant issue in modern programming languages is unsafe aliasing. Modern type systems have attempted to address this in two prominent ways; immutability and ownership, and often a combination of the two [4][17]. The goal of this thesis is to formalise Immutability and Ownership using the Coq Proof Assistant, a formal proof management system [13]. We encode three type systems using Coq; Featherweight Immutable Java, Featherweight Generic Java and Featherweight Ownership Generic Java, and prove them sound. We describe the challenges presented in encoding immutability, ownership and type systems in general in Coq.</p>

True Concurrency Semantics

2014 ◽  
Vol 5 (2) ◽  
pp. 22-42 ◽  
Author(s):  
Souad Guellati ◽  
Ilham Kitouni ◽  
Riad Matmat ◽  
Djamel-Eddine Saidouni
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Timed Automata ◽  
Model Data ◽  
True Concurrency ◽  
New Class ◽  
Computation Tree ◽  
Interleaving Semantics ◽  
Finite State ◽  
Validation Technique

The model checking algorithms have been widely studied for timed automata, it's a validation technique for automatically verifying correctness properties of finite-state systems, which are based on interleaving semantics. Therefore the actions are assumed instantaneous. To overcome the hypothesis of temporal and structural atomicity of actions, we use the durational actions timed automata model (daTA). This model is based on the maximality semantics. Properties to be verified are expressed using the Timed Computation Tree Logic (TCTL). For dealing with formal verification, the Maximality-based Region Graph (MRG) is defined and an adaptation of the model checking algorithm is proposed. The use of the maximality semantics based verification provides new class of properties related to simultaneous progress of actions at different states.

scholarly journals The Marriage of Univalence and Parametricity

2021 ◽  
Vol 68 (1) ◽  
pp. 1-44
Author(s):  
Nicolas Tabareau ◽  
Éric Tanter ◽  
Matthieu Sozeau
Keyword(s):  
Type Theory ◽  
Program Verification ◽  
Proof Assistants ◽  
Computationally Efficient ◽  
Lightweight Framework ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant ◽  
Efficient Representation ◽  
Term Dependency ◽  
Work First

Reasoning modulo equivalences is natural for everyone, including mathematicians. Unfortunately, in proof assistants based on type theory, which are frequently used to mechanize mathematical results and carry out program verification efforts, equality is appallingly syntactic, and as a result, exploiting equivalences is cumbersome at best. Parametricity and univalence are two major concepts that have been explored in the literature to transport programs and proofs across type equivalences, but they fall short of achieving seamless, automatic transport. This work first clarifies the limitations of these two concepts when considered in isolation and then devises a fruitful marriage between both. The resulting concept, called univalent parametricity , is an extension of parametricity strengthened with univalence that fully realizes programming and proving modulo equivalences. Our approach handles both type and term dependency, as well as type-level computation. In addition to the theory of univalent parametricity, we present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. For instance, this makes it possible to conveniently switch between an easy-to-reason-about representation and a computationally efficient representation as soon as they are proven equivalent. The combination of parametricity and univalence supports transport à la carte : basic univalent transport, which stems from a type equivalence, can be complemented with additional proofs of equivalences between functions over these types, in order to be able to transport more programs and proofs, as well as to yield more efficient terms. We illustrate the use of univalent parametricity on several examples, including a recent integration of native integers in Coq. This work paves the way to easier-to-use proof assistants by supporting seamless programming and proving modulo equivalences.

Sign in / Sign up

Export Citation Format

Share Document