CakeML
About CakeML is a functional programming language and an ecosystem of proofs and tools built around the language. The ecosystem includes a proven-correct compiler that can bootstrap itself. The CakeML project consists of the following components, all of which are free software. Language definition. The CakeML language is based on a substantial subset of Standard ML. Its formal semantics is specifi
Isabelle入門の入門 - Qiita
最近Isabelle始めたばかりなので, 初心者的な視点からIsabelle入門以前の話をします. この記事を読んでIsabelleに興味を持たれたら, 是非公式turtorialからIsabelleへ入門してみてください. Isabelleについて Isabelleは証明支援言語です. 以下にその特徴をあげてみます. 標準のjEdit環境がリッチ 強力な自動証明機構 (とにかく自動証明コマンドが豊富で, さらに証明をIsabelleに探索させることもできます) 公理系が選べる (公理系はライブラリレベルでサポートされています. importするライブラリを自分で選ぶことで, HOL, ZF, Sequents, Cube などなどたくさんの公理系を扱うことができます) Isabelle/Isarによる人間に優しい証明 (Coqのように証明図をコマンドによって変形していくだけでなく, Is
Lean Programming Language
Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code -- 'Grind' efficiently manages complex pattern matching and -- case analysis beyond standard tactics. example (x : Nat) : 0 < match x with | 0 => 1 | n+1 => x + n := by grind -- Automatically solves systems of linear inequalities. example (x y : Int) : 27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 4
#TPP2014 高信頼な理論と実装のための定理証明および定理証明器
研究集会 「高信頼な理論と実装のための定理証明および定理証明器」 高信頼なソフトウェア開発のために必要な形式手法, ソフトウェア検証, 数学の形式化, および, 証明の計算機による検証に関する研究集会を九州大学西新プラザで開催します. 続きを読む
TPTP Services are Down
Why are you looking for the TPTP on this server? Try www.tptp.org
Mizar - Wikibooks
このページ「Mizar」は、まだ書きかけです。加筆・訂正など、協力いただける皆様の編集を心からお待ちしております。また、ご意見などがありましたら、お気軽にトークページへどうぞ。
Mizar - Wikipedia
自動証明検証システム Mizar（ミザー、ミザール）は、まったく厳密に形式的な形で数学的な定義や証明を記述するためのデータ記述言語（Mizar-言語）、実際にその言語で記述された証明の内容を検証することができる計算機プログラム（証明検証プログラム）、プログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理からなるライブラリ (MML) の三者から構成される。 Mizar と同様の目的を持つプロジェクトに、ロバート・ボイヤーのQEDプロジェクトがある。 システムの開発は1973年にアンジェイ・トリブレッツによって始められ、システムの保守をポーランドのビアリストーク大学（英語版）、カナダのアルバータ大学、日本の信州大学で行っている。 Mizar-言語で記された証明文（以下、Mizar-論文）は普通のASCIIコードで書かれている。Mizar-言語は、数学の通常の言葉遣いと書式がよく
Prototype Verification System (PVS)
PVS is a mechanized environment for formal specification and verification. PVS consists of a specification language, a large number of predefined theories, a type checker, an interactive theorem prover that supports the use of several decision procedures and a symbolic model checker, various utilities including a code generator and a random tester, documentation, formalized libraries, and examples
ACL2 Version 2.9 ACL2 is both a programming language in which you can model systems and a tool to help you prove properties of those models. lisp
Welcome to the ACL2 home page! We highlight a few aspects of ACL2: Libraries (Books). Libraries of books (files containing definitions and theorems) extend the code that we have written. In particular, the distribution tarball includes the community books, which are contributed and maintained by the members of the ACL2 community. Documentation. There is an extensive user's manual for the ACL2 syst
WebHome < Mizar < TWiki
Mizar TWiki The Mizar web is the main collaboration area for people using the Mizar proof checker and people involved in its implementation or implementation of related software. Please do not hesitate to add/edit as many pages as you can Hint: Subscribe to WebNotify to be automatically notified when something changes in the TWiki.Mizar web Mizar Questions and Hints InstallationAndFirstArticle: Mi
ProVerif
ProVerif: Cryptographic protocol verifier in the formal model ProVerif is an automatic cryptographic protocol verifier, in the formal model (so called Dolev-Yao model). This protocol verifier is based on a representation of the protocol by Horn clauses. Its main features are: It can handle many different cryptographic primitives, including shared- and public-key cryptography (encryption and signat
miTLS - Home
miTLS is a verified reference implementation of the TLS protocol. Our code fully supports its wire formats, ciphersuites, sessions and connections, re-handshakes and resumptions, alerts and errors, and data fragmentation, as prescribed in the RFCs; it interoperates with mainstream web browsers and servers. At the same time, our code is carefully structured to enable its modular, automated verifica
Gabriel Gonzalez 氏の Equational Reasoning を読んだメモ - relations -> transitive
自分も「プログラマのための等式推論」的な記事書いてみたいとか思っていて、手頃な記事を氏が最近書かれていたのを思い出し、注意深く読むことにした。素人がちょっと分かったつもりになると人に教えたがるアレな病気を発症してるのです。 Haskell for all: Equational reasoning 手で式を置き換えることによって Haskell のコードは解釈できる 等式から等式へ置き換えて式を解釈することを等式推論 (equational reasoning) という Haskell では左辺と右辺は相互に置換可能 x = 5 という宣言をしたとする。このときプログラム中に x を見つけたら機械的に 5 に置き換えてよい (substitution) 。同様に 5 を見つけたら x に置き換えてよい Haskell ではこのような置き換えを行ってもプログラムのふるまいは変わらない (参照
sbv
sbv: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Express properties about Haskell programs and automatically prove them using SMT (Satisfiability Modulo Theories) solvers. [Skip to Readme] DataData.SBVData.SBV.CharData.SBV.ControlData.SBV.DynamicData.SBV.EitherData.SBV.FloatData.SBV.InternalsData.SBV.ListData.SBV.MaybeData.SBV.RationalData.SBV.RegExpData.SBV.SetData.
Proof Market
This is a proof market for Coq. The list of all problems Create a new problem Recent answers How to get proofs done for bitcoins Create a new problem wait for somebody to solve the problem on recent entries pay bitcoins see the proof How to get bitcoins for proving find a problem on the list of all problems (optional) contact possible payers solve the problem post your solution with a price and yo
定理証明系 Haskell
この記事は Haskell Advent Calendar 2013 および Theorem Prover Advent Calendar 2013 二十日目の記事であり、更にTCUGの新刊「Coqによる定理証明」の販促記事でもある。 型システム再考 Haskell は静的型付き言語だ。それだけでなく、強力な型推論や表現力の高い型システムを備えている。 型とは何だろうか。 こうした質問に対してよくある答えは、「値の種類を区別するためのタグ」になるだろうか。Int型は整数だし、Bool型は真偽値で、[Int]型は整数値リストを表す型だ。なるほど、値の種類を区別するものに見える。 しかし、この答えは間違ってはいないが、もっと相応しい云い方が出来るだろう。それは、「型は不変条件である」というものだ1。この言明は別に私固有の見方というわけではなく、ある程度の型レベルプログラミングをやった事のある人
Matita - Home Page
27 Dec 2017 The repository of Matita has now migrated to Git. See the download page for further infos. 18 May 2016 Matita release 0.99.3 available for download. 23 December 2014 Legacy matita release 0.5.9 available for download. 13 March 2012 The Matita web app is now publicly accessible online (go). 13 March 2012 Matita release 0.99.1 available for download. 1 February 2010 Project CerCo (Certif
プログラムに証明が付く日 | RANDMAX
この記事は「Theorem Prover Advent Calendar 2013」6日目の記事です。 http://qiita.com/advent-calendar/2013/theorem_prover 神田「野らぼー」にて、地下の薄暗い店内で… 「そう言えばこないだ隣で起こってたポインタオーバーラン、対応大変そうだったですけどちゃんと家に帰れてたんでしょうかね、新婚なのに…」 「ヌルポとかポインタオーバーランとか、どうして無くならないんだろうね。その時はみんな手を抜いてるつもりなんて毛頭なくて、一生懸命考えて大丈夫だと思ってるはずなんだけどね。レビューもして、それでも起こった後でみんなでソース見てみると、なんで気づかなかったんだよ！ってことになる。」 「人間って、そういうの苦手なんでしょうねきっと。ほら、『何かほかにありませんか』って聞かれても出てこないじゃないですか。静的な解析っ
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
ProofSummit2014 : VSTでCの検証
ProofCafe - Schedule/ProofSummit2014