I came upon the Curry-Howard Isomorphism relatively late in my programming life, and perhaps this contributes to my being utterly fascinated by it. It implies that for every programming concept there exists a precise analogue in formal logic, and vice versa. Here's a "basic" list of such analogies, off the top of my head: program/definition | proof type/declaration | proposition inhabited type | t
I’m a fan and long-term user of the Isabelle/HOL proof assistant. More recently I have been studying Lamport’s TLA+ system which is a popular choice for writing specifications of systems. This post is a slightly tidied-up version of some notes about my early experiences of playing with the implementation of TLA within Isabelle/HOL, to record a handful of obstacles I hit and some techniques I found
[2023-02-24 Fri]: Ubuntu 22.04.1 LTS, Coq 8.16.1, MathComp 1.16 [2023-01-06 Fri]: Ubuntu 22.04.1, opam 2.1.4, ocaml 4.14.1, Coq 8.16.1, ProofGeneral 4.6, MathComp 1.15.0, MathComp-Analysys 0.6.0 [2022-09-09 Fri]: Ubuntu 22.04.1, Coq 8.15, MathComp 1.15 (opam), ProofGeneral 4.6 [2022-08-03 Wed]: Windows 11, Coq 8.15, MathComp 1.15 (WSL 2) [2022-03-01 Tue]: Windows 11 21H2, Coq 8.15, MathComp 1.14 (
index : kernel/git/cmarinas/kernel-tla.git Kernel TLA+ specsCatalin Marinas aboutsummaryrefslogtreecommitdiffstats BranchCommit messageAuthorAge masterasidalloc: Fix inadvertently removed line from UniqueASIDActiveTaskCatalin Marinas3 years AgeCommit messageAuthorFilesLines 2021-09-10asidalloc: Fix inadvertently removed line from UniqueASIDActiveTaskHEADmasterCatalin Marinas1-17/+19 2021-08-05asid
Coq のカリー・ハワード同型周辺についてメモ.間違いあればご指摘ください. Coq と CoC Coq は元々,Thierry Coquand 氏により提案された Calculus of Constructions (CoC) という型システムの実装として生まれました. その後 CoC は,帰納的データ型などが追加された Calculus of Inductive Constructions (CIC) に拡張され,現在の Coq は CIC の実装となっています. CoC/CIC は,基本的には型システムを定義しただけのものなのですが,実は Coq の証明システムはこの型システムがベース となっています. これは一体どういうことか,次からの節で,直観的な例を通して見ていくことにします. プログラム ≈ 証明 一般に,プログラムの型システムは,次の図みたいな推論木を組み立ててプログラムの
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く