All Projects → sfja → Sfja

sfja / Sfja

Licence: mit
SoftwareFoundations(Ja)

Labels

Projects that are alternatives of or similar to Sfja

Coq Printf
Implementation of sprintf for Coq
Stars: ✭ 15 (-76.92%)
Mutual labels:  coq
Freespec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 41 (-36.92%)
Mutual labels:  coq
Perennial
Verifying concurrent crash-safe systems
Stars: ✭ 57 (-12.31%)
Mutual labels:  coq
Profunctor Monad
Bidirectional programming in Haskell with monadic profunctors
Stars: ✭ 30 (-53.85%)
Mutual labels:  coq
Parseque
Total Parser Combinators in Coq
Stars: ✭ 37 (-43.08%)
Mutual labels:  coq
Poleiro
A blog about Coq
Stars: ✭ 42 (-35.38%)
Mutual labels:  coq
Hello World
A Hello World program in Coq.
Stars: ✭ 14 (-78.46%)
Mutual labels:  coq
Riscv Coq
RISC-V Specification in Coq
Stars: ✭ 63 (-3.08%)
Mutual labels:  coq
Certint
A Certified Interpreter for ML with Structural Polymorphism
Stars: ✭ 39 (-40%)
Mutual labels:  coq
Verlang
Stars: ✭ 52 (-20%)
Mutual labels:  coq
Nuprlincoq
Implementation of Nuprl's type theory in Coq
Stars: ✭ 31 (-52.31%)
Mutual labels:  coq
Compcert
The CompCert formally-verified C compiler
Stars: ✭ 984 (+1413.85%)
Mutual labels:  coq
Metalib
The Penn Locally Nameless Metatheory Library
Stars: ✭ 47 (-27.69%)
Mutual labels:  coq
Hott
Homotopy type theory
Stars: ✭ 946 (+1355.38%)
Mutual labels:  coq
Scala Escape
A compiler plug-in to control object lifetimes in Scala
Stars: ✭ 60 (-7.69%)
Mutual labels:  coq
Vvclocks
Verified vector clocks, with Coq!
Stars: ✭ 14 (-78.46%)
Mutual labels:  coq
Pornview
Porn browser formally-verified in Coq
Stars: ✭ 42 (-35.38%)
Mutual labels:  coq
Scallina
A Coq-based synthesis of Scala programs which are correct-by-construction
Stars: ✭ 65 (+0%)
Mutual labels:  coq
Collapsing Towers
Collapsing Towers of Interpreters
Stars: ✭ 61 (-6.15%)
Mutual labels:  coq
Silveroak
Formal specification and verification of hardware, especially for security and privacy.
Stars: ✭ 51 (-21.54%)
Mutual labels:  coq

Sfja - Software Foundations (ja)

Build status

CircleCI

Contributions

発起人の片山です。4章までの翻訳を行いました。

以下は、梅村氏との質疑で出た、現状の翻訳方針です。 決定事項というわけではありませんが、特に「こうしたほうがいい」という ことがなければ、当面文体などはこの方針でお願いいたします。

・文体は「ですます」調。ただし定理の主張の訳や、証明に直接付加され た説明は、「示す」「とする」「になる」等の文体とする。また、  練習問題は、「しなさい」という命令調のほうが気分がでるのでそう  する。ただし、練習問題の説明はですますで書く。

・句読点は「、」「。」 (「,」「.」ではないという意味)     ・英語版の.vのソースファイル上では、半角80で改行が入っていますが、  日本語のコメントでこれをやってしまうとhtmlに変換した際に半角  スペースが入ってしまうので、日本語の.vファイルでは改行をいれずに  ダラダラ書いてください。

・原文冒頭の (* $Date: ...$ *) はそのまま(もとの日付のまま)残す  (いつの版の翻訳か分かるように)。

  ・原文で XXX という部分は、その場所ごとに適切に対処(オリジナル  ではイタリック体にする記号だが、最初の4章までは無視している  (日本語がアンダーラインに続くとうまくcoqdocが処理してくれない   ため)。   ・原文の"XXX" は基本的には,中のXXXは訳すがダブルクォートはそのまま 残して"YYY"とする。ただし、日本語にして違和感がある場合は  「」で置き換えてもかまわない。   ・原文の[XXX]は中のXXXも訳さずにそのまま[XXX]とする。たいていは  ソースの中のキーワードや変数名などに使われているので、必然的に  そうなると思います。 ・ダッシュ (-) で始まる行はなるべく原文のままの形のインデントを残す。

・コメントではない部分は基本的に原文のままとする。

他にも何か気づいたことがあれば追加してください (以上:2011/10/01 片山)

同じところを同時に複数の人が翻訳してしまう悲劇を防ぐため、念のため、 自分が翻訳を開始している章は、Wiki上に「****が翻訳中」と 記述するようにして下さい。

また、翻訳方針などについて、統一を求めたい場合はこのファイルに追記 してください。

単語の訳語の統一については、Wikiのほうで単語帳を管理することにしましょう。 (例:tactic → タクティク × タクティック ○ など)

(以上:2011/10/02 片山)

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].