scholarly journals Verification of a brick Wang tiling algorithm

10.29007/2m5f ◽  
2018 ◽  
Author(s):  
Toshiaki Matsushima ◽  
Yoshihiro Mizoguchi ◽  
Alexandre Derouet-Jourdan
Keyword(s):  
Computer Graphics ◽  
Proof Assistant ◽  
Induction Process ◽  
Coq Proof Assistant ◽  
Wang Tile

We have implemented a certified Wang tiling program for tiling a rectangle region using a brick corner Wang tile set. A brick corner Wang tile set is a special Wang tile set introduced by A. Derouet-Jourdan et al. in computer graphics in 2015 to model wall patterns texture. We have implemented a tiling algorithm using Coq proof assistant and proved its correctness. This correctness assures the existence of a tiling of any brick corner Wang tile set for any size of rectangle. The essential points of our proof are the existence of a tiling for a $2 \times 2$ rectangle and a simple induction process. Since the brick corner Wang tile is a class of infinite kinds of tile sets, it is not straightforward and there are many conditional branches to prove the correctness. The certification with Coq assures that there are no lack of conditions.

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.

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 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>

scholarly journals An experimental library of formalized Mathematics based on the univalent foundations

2015 ◽  
Vol 25 (5) ◽  
pp. 1278-1294 ◽  
Author(s):  
VLADIMIR VOEVODSKY
Keyword(s):  
Type Theory ◽  
Proof Assistant ◽  
Formalization Of Mathematics ◽  
Constructive Type Theory ◽  
Short Overview ◽  
Formalized Mathematics ◽  
The Coq Proof Assistant ◽  
Constructive Type ◽  
Coq Proof Assistant ◽  
Univalent Foundations

This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).

scholarly journals Tactic Learning and Proving for the Coq Proof Assistant

10.29007/wg1q ◽  
2020 ◽  
Author(s):  
Lasse Blaauwbroek ◽  
Josef Urban ◽  
Herman Geuvers
Keyword(s):  
Machine Learning ◽  
Proof Assistant ◽  
Proof Search ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant ◽  
Two Systems ◽  
Similar Vein ◽  
Standard Library

We present a system that utilizes machine learning for tactic proof search in the Coq Proof Assistant. In a similar vein as the TacticToe project for HOL4, our system predicts appropriate tactics and finds proofs in the form of tactic scripts. To do this, it learns from previous tactic scripts and how they are applied to proof states. The performance of the system is evaluated on the Coq Standard Library. Currently, our predictor can identify the correct tactic to be applied to a proof state 23.4% of the time. Our proof searcher can fully automatically prove 39.3% of the lemmas. When combined with the CoqHammer system, the two systems together prove 56.7% of the library’s lemmas.

Sign in / Sign up

Export Citation Format

Share Document