準同型写像に関する定理 [物理のかぎしっぽ]
群 が群 の上へ準同型写像で移されるときの核を とします．そして，この写像によって， の元 が に移されるとします．しかし，逆に に対応する の元が だけとは限りません(全射の図を思い出してください)． に移される元だけを集めると，この集合は の による剰余類 に等しい，という性質があります． theorem 群 の群 の上への準同型写像の核を とします．また，この写像によって， の元 は に移されるとします．このとき， に移される の元の集合は， です． proof 二つの元 がともに に移されるとします． ．このとき，準同型写像によって逆元は逆元に移されることを使って が言えます．よって定義より が分かりますから，両辺に を掛けて が言えます．■
Wadler: Call-by-value is dual to call-by-name
Philip Wadler Down with the bureaucracy of syntax! Pattern matching for classical linear logic Philip Wadler. Draft. This paper introduces a new way of attaching proof terms to proof trees for classical linear logic, which bears a close resemblance to the way that pattern matching is used in programming languages. It equates the same proofs that are equated by proof nets, in the formulation of pro
Getting started
The Coq Proof Assistant A Tutorial Version 1 Gérard Huet, Gilles Kahn and Christine Paulin-Mohring LogiCal Project 1This research was partly supported by IST working group “Types” Getting started Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs
Coq for POPL folk
Using Proof Assistants for Programming Language Research or, How to write your next POPL paper in Coq San Francisco, CA January 8th, 2008 A tutorial on the use of the Coq proof assistant in formalizing programming language metatheory. This tutorial will be tailored to people who are familiar with syntactic proofs of programming language metatheory, such as type soundness, but have never used a pro
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
