ikedaisuke

Search lemma on the fly in ProofGeneral

A helm extension for Search command.

/disambiguation/

• in the text, helm means Emacs-helm
• not means the HELM library of mathematics.

ikedaisuke

;; How to use:
;; impatient-mode
;; M-x imp-set-user-filter
;; markdown-filter
;; see also https://github.com/skeeto/impatient-mode
(defun markdown-filter (buffer)
  "Render a markdown document on your browser in real time by impatient-mode and markdown-mode."
  (princ
   (with-temp-buffer
     (let ((tempname (buffer-name)))

ikedaisuke

Emacs の git クライアント magit の個人的なまとめです。正確かどうかは保証しません。

こんな cheat sheet を参照するくらいなら magit の公式ドキュメント読んだほうがいいと思う。

Magit!

バージョン

git

ikedaisuke

-- % idris simple-uniq.idr -o uniq
module Main

getContents : IO String
getContents = go ""
  where go : String -> IO String
        go s = do case !(feof stdin) of
                    True  => return s
                    False => do t <- fread stdin
                                go (s ++ t)

ikedaisuke

Real world (functional) programming with dependent types!
---------------------------------------------------------
* we want to write a program with /dependent types/
  * shallow embedding vs. deep embedding
* we want to prove some properties of each part of the program
* we need reasoning about programs
  * especially, a program will run correctly
    * interactiton with I/O
    * mutable state
    * etc.

ikedaisuke

ぷるーふさみっと2015、ライトニングトーク、ラジオー（仮）の台本

みなさん、こんにちは、「発表者」です。 この番組ではリスナーの皆さんに「定理証明」の話題をお届けいたします。 たぶん、今回が最初で最後だと思います。

これから15分ほどの間、お付き合いくださいませ。

それではさっそくメールを読み上げていきたいと思います。 ラジオネーム「とあるHaskell golfer」さんから質問をいただきました。

ikedaisuke

; try the following code at http://rise4fun.com/z3/tutorial
; data type Nat
(declare-datatypes () ((Nat zero (succ (pred Nat)))))
; plus as a rule
(declare-fun plus (Nat Nat Nat) Bool)
; rule P-Zero
(assert (forall ((n Nat)) (plus zero n n)))
; rule P-succ
(assert (forall ((m Nat) (n Nat) (r Nat))
  (=> (plus m n r) (plus (succ m) n (succ r)))))

ikedaisuke

# Current Trends on Gröbner Bases 関連文書まとめ

The 8th Mathematical Society of Japan Seasonal Institute
Current Trends on Gröbner Bases
— The 50th Anniversary of Gröbner Bases —

July 1 - July 10, 2015 

http://www.math.sci.osaka-u.ac.jp/~msj-si-2015/index.html

ikedaisuke

Ruby の Array は関数型プログラミングの List とは違います。

が、Ruby 1.8.7 以上で Enumerable は大きく変わりました。
その結果、関数型プログラミングの文脈における List のかなりのことが、
短いプログラム断片で書けるようになったと理解しています。

関数型プログラミングでは、さらに List を抽象化できます。
その一つが Rose tree [Bird 1998] です。

Ruby でも、このような抽象化があれば役にたつと思います。

ikedaisuke

説明はあとで（適当に）します。 このファイルを protocol.pml という名前で保存して、次の手順を踏みます：

> spin -a protocol.pml
> gcc pan.c
> ./a.out
> spin -M -t protocol.pml

以上で protocol.pml.ps という PostScript ファイルができあがります。