Translating the Michelson interpreter | Coq Tezos of OCaml 💫
Verifying the implementation of the interpreter of Michelson smart contracts is of importance because one of the strengths of Tezos is to be able to formally verify the smart contracts. In order to make this verification sound, we need to show that the smart contracts verification framework 🍬 Mi-Cho-Coq is coherent with the actual implementation of Michelson. In this blog post, we show how we tra
GitHub - magmide/magmide: A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
🚧 Magmide is purely a research project at this point 🚧 This repo is still very early and rough, it's mostly just notes, speculative writing, and exploratory theorem proving. Most of the files in this repo are just "mad scribblings" that I haven't refined enough to actually stand by! If you prefer video, this presentation talks about the core ideas that make formal verification and Magmide possib
最小共通祖先を求めるアルゴリズムの形式検証 | Wantedly Engineer Blog
競技プログラミングには概念を知っておかないと解きようがない、いわゆる覚えゲーのような問題が存在します。典型的な例が 10^9+7 といった素数で割った余りを求めろといったもので、普段業務で日常的に素数で割った余りを求めている人でもなければ、割り算がしたければフェルマーの小定理や拡張ユークリッドの互除法を使えば良いと直ぐには思い付けないのではないでしょうか。 最小共通祖先も覚えゲーで必要な概念の一種と言えます。これは読んで字のごとく、与えられた根付き木の下で2頂点に共通する祖先のうち、最も根から遠い頂点を指す概念で、例えば木の2頂点が与えられて、頂点間の経路について何かを求めろといった問題で威力を発揮することが多いです。これを用いて解ける例を挙げるとすると次の問題でしょうか。 https://atcoder.jp/contests/abc014/tasks/abc014_4 最小共通祖先を求
Translating My Z3 Tutorial to Coq
I had a fun time giving a Z3 tutorial at Formal Methods for the Informal Engineer (FMIE) https://fmie2021.github.io/ (videos coming soon hopefully!). I got to be kind of the "fun dad" with the Z3 tutorial https://github.com/philzook58/z3_tutorial , while at times it felt a bit like Cody's Coq tutorial https://github.com/codyroux/broad-coq-tutorial was trying to feed the kids their vegetables. It w
ML のサブセットの型推論器を Coq で検証する - fetburner.core
この記事は言語実装 Advent Calendar 2020 の5日目の記事です． 一度でも型推論器を書いたことがあれば，そのあまりの邪悪さ，あるいはその複雑さに恐れ慄いたことでしょう． 参照を用いて単一化を実現しようものなら構文木は参照に汚染され，純粋関数型に実装しようものなら大量の型代入をどのような順序で適用したものか悩まされる． これは Hindley-Milner 型推論器を実装する上での宿命のようなものです． 本記事では，MLのサブセット——型付きλ計算をletと参照で拡張した，let多相をサポートする言語——の型推論器を Coq で実装し，その正当性を証明します． Coq で検証を行うことで我々は型推論器のバグへの恐怖とデバッグの労力から真に解放され，枕を高くして眠ることができることでしょう． もっとも、型付きλ計算を let 多相で拡張した言語の型推論器の正当性は実はすでに証
TopProver
Coq competition Coq をはじめとする証明支援システムを用いるコンテストサイトです 出題を希望して下さる方や、質問,要望,バグ報告などご用のある方は、@asi1024 までご連絡お願いします。 初心者の方は 環境準備: CoqIDE (公式サポートの対話型証明アシスタント) を使う場合 GitHub のリリースページ: The release page on GitHub CoqIDE を使わない場合 Coq のインストール: Install Coq with opam 対話型証明アシスタントの導入 Proof General (Emacs) vscoq (Visual Studio Code) 有名な教材: Software Foundations その他 FAQ 利用規約 採点環境の Coq のバージョンアップデートについて (2020/05/03)
Gopiandcode > logs > Bloom filters debunked: Dispelling 30 Years of bad math with Coq!
There's this rather nifty feature of modern web browsers (such as Firefox or Chrome) where the browser will automatically warn the user if they happen to navigate to a "malicious" URL: While conceptually simple, this feature actually requires more engineering effort than one would expect - in particular, tracking the set of known malicious URLs in a practical manner turns out to be somewhat diffic
クイックソートは半順序でもソート可能であることをCoq/SSReflectで証明する - Qiita
はじめに 前回の記事で、全順序が仮定されているからこそうまくいくソートアルゴリズムを半順序で使用するとどうなるかを見ました。結果としてクイックソートなら半順序でもうまくソートできることを見ましたが、本記事では、これを定理証明支援系Coqを用いて、形式的に証明していきます。 定理証明支援系Coqに関して軽く説明しておくと、プログラムが正しく動くことを、数学的に検証できるツールとして使えるものです。 クイックソートを定義 SSReflectのpathライブラリには、標準のソート関数sortが定義されていますが、このアルゴリズムはマージソートなので、前回の記事で検証したように半順序では使えません。 そこでCoqでクイックソートを定義します。 まず定義の前に、ソートを行う要素の集合Tと、半順序関係Rを宣言しておきます。実際にはTは型で、RはただのT上の二項関係T -> T -> boolとして定義
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - thaliaarchi/bfcoq: Brainfuck compiler in Coq
GitHub - logsem/aneris: Program logic for developing and verifying distributed systems
GitHub - artagnon/bonak: 🧊 An indexed construction of semi-simplicial and semi-cubical types
Untangling mechanized proofs
GitHub - stepchowfun/proofs: My personal repository of formally verified mathematics.
Reflexive tactics for algebra, revisited
Coq Platform 2022.01.0
On relational compilation
Formalizing Dawn in Coq
GitHub - jonsterling/coq-domains
Proving Algebraic Datatypes are “Algebraic”
Deep dive into Meta-Theory à la Carte (part 1) - Coq en Stock