Coqはチューリング完全 -- Ltacでbrainf*ckインタプリタを書いた - Qiita
この記事は、Theorem Prover Advent Calender https://qiita.com/advent-calendar/2017/theorem-prover のために書かれました。 Coqをある程度知っている人向けの小ネタです。 しばしばCoqの紹介において、「Coqでは停止するプログラムしか書けない」「(そのため)Coqはチューリング完全ではない」と言われることがあります。実はこれ、正しいと言えば正しいのですが、間違いと言えば間違いです。 確かに、Coqで再帰関数を定義するためのFixpoint, Program Fixpoint, Functionといったコマンドはどれも停止性を要求します。そのため、Coqから抽出したプログラムは無限ループを起こすことはなく、その意味で安全性が保証されることになります。 では、何が間違いか？ これは「Coqでは停止するプログラム
dbp.io :: How to prove a compiler correct
How to prove a compiler correct At POPL’18 (Principles of Programming Languages) last week, I ended up talking to Annie Cherkaev about her really cool DSL (domain specific language) SweetPea (which she presented at Off the Beaten Track 18, a workshop colocated with POPL), which is a “SAT-Sampler aided language for experimental design, targeted for Psychology & Neuroscience”. In particular, we were
Rust's ownership model formally proven with Coq | Lobsters
source tweet PDF paper In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verific
https://www.irif.fr/~sozeau//research/publications/drafts/Towards_Certified_Meta-Programming_with_Typed_Template-Coq.pdf
Towards Certified Meta-Programming with Typed Template-Coq Abhishek Anand1 , Simon Boulier2 , Cyril Cohen3 , Matthieu Sozeau4 and Nicolas Tabareau2 1 Cornell University, Ithaca, NY U.S.A. 2 Gallinette Project-Team, Inria Nantes, France 3 Université Côte d’Azur, Inria, France 4 Pi.R2 Project-Team, Inria Paris and IRIF, France Abstract. Template-Coq5 is a plugin for Coq, originally implemented by
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code
Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell's containers library into Coq, and verify it against specifications that we derive from a variety of sources including type class laws, the library's test suite, and interfaces from Coq's standard library. Our work shows that it is feasi
C2TLA
& www.cea.fr C2TLA+: A translator from C to TLA+ Amira METHNI (CEA/CNAM) Matthieu LEMERRE (CEA) & Belgacem BEN HEDIA (CEA) Serge HADDAD (ENS Cachan) & Kamel BARKAOUI (CNAM) June 3, 2014 Cliquez pour modifier le style du titre DACLE Division| June 2013 © CEA. All rights reserved | 2 & Outline Introduction General approach Translation from C to TLA+ Memory model Expressions Intra-procedural control
Modeling Redux with TLA+
New: My new book, Logic for Programmers, is now in early access! Update 01/07/19 Greetings from 2019! The good news is that Chicago isn’t yet a radioactive crater. The bad news is almost everything I said about refinement in this article is wrong. I’m working on writing a more in-depth, rigorous treatment of refinement as its own article. But this one is currently explaining something that definit
Modeling Redux with TLA+
New: My new book, Logic for Programmers, is now in early access! Update 01/07/19 Greetings from 2019! The good news is that Chicago isn’t yet a radioactive crater. The bad news is almost everything I said about refinement in this article is wrong. I’m working on writing a more in-depth, rigorous treatment of refinement as its own article. But this one is currently explaining something that definit
The TLA+ Home Page
Leslie Lamport Last modified on Fri 1 March 2024 at 16:38:51 PST by lamport --> This is the home page of the TLA+ web site. TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones. It's based on the idea that the best way to describe things precisely is with simple mathematics. TLA+ and its tools are useful for eliminating fundamental design er
Leslie Lamport's Home Page
My Coordinates 37° 24' 14" North 122° 2' 6" West address: Microsoft Corporation 1020 Enterprise Way Sunnyvale, CA 94089 U.S.A. email: I am happy to receive email from people, but not from spammers. So, please do not put my email address on the Web in plain text. You may post this gif file if you wish.
トップ エスイー
入社以来の研究分野（ハード開発）からソフトウェアの世界に転向した際に，上司から勧められたことが受講のきっかけでした．独学では得難い，ソフトウェア工学の体系だった理解を得ることができたと思っています. 修了生の声(対談)(2023/11/24 トップエスイー第19期生向け講座説明会にて) 15期生 富士通株式会社 鳥野剛史 15期生 株式会社NTTデータグループ 呉隆司 17期生 キヤノン株式会社 野澤友暉 More Topics トップエスイーの成果はどうなのか？ 修了生の声をご覧ください． トップエスイー紹介動画がYouTubeでご覧いただけます． 月刊「先端教育」2022年10月号にトップエスイーの記事が掲載されました． 記事の抜粋はこちらからご覧いただけます（2022-11-14）
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - sweirich/corespec: A Specification for Dependent Types in Haskell (Core)
Koichi Hatanaka on Twitter: "IBM Developer Advocate の 「IBM だチャンネル podcast」の、第7回はDeveloper向けコミュニティの紹介。 18分で、Bluemix Users Group、Node-RED User... https://t.co/EUbsad6tlA"
https://sites.google.com/site/disbookalo1973/2018-01-24---21-54-01--239/Skachat_programma_dlia_ia_soromlius_svogo_tla_2_sezon_iutub.pdf?attredirects=0
https://sites.google.com/site/fecgemetol1971/2018-01-25---14-04-19--483/Skachat_programma_dlia_ia_soromlius_svogo_tla_3_sezon_6_vypusk.pdf?attredirects=0
the passing bells s01e05 720p hdtv x264 tla
lewis s08 tla
Lamport talk
https://lamport.azurewebsites.net/tla/book-02-08-08.pdf
Infer Static Analyzer - Wikipedia