# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1486965606 -32400
# Node ID 4e30a8a7128c561399c21dba2a5d8114d1d006f6
# Parent  a133c32db45ee73c5b1a809cf0280ed494877877# Parent  5ad74fb83f722fb45b11da64ba355f651be7db57
Merge

diff -r a133c32db45e -r 4e30a8a7128c paper/atton-master.pdf
Binary file paper/atton-master.pdf has changed
diff -r a133c32db45e -r 4e30a8a7128c paper/cbc-type.tex
--- a/paper/cbc-type.tex	Mon Feb 13 14:59:25 2017 +0900
+++ b/paper/cbc-type.tex	Mon Feb 13 15:00:06 2017 +0900
@@ -1,4 +1,4 @@
-\chapter{Agda における Continuation based C の表現}
+\chapter{Agda による Continuation based C の表現}
 \label{chapter:cbc-type}
 ~\ref{chapter:agda}章では Curry-Howard 同型対応により、型付きラムダ計算を用いて命題が証明できることを示した。
 加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。
@@ -6,7 +6,7 @@
 CbC で自身を証明するために依存型を利用したいが、CbC には専用の型システムが存在しない。
 依存型をCbCコンパイラで扱うためにもまず現状の CbC を型付けする必要がある。
 
-~\ref{chapter:cbc-type}では CbC の項が部分型で型付けできることを示す。
+~\ref{chapter:cbc-type}章では CbC の項が部分型で型付けできることを示す。
 定義した型システムを用いて、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、それらが型付けされることを確認する。
 また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda で証明する。
 
diff -r a133c32db45e -r 4e30a8a7128c paper/src/AgdaModusPonens.agda
--- a/paper/src/AgdaModusPonens.agda	Mon Feb 13 14:59:25 2017 +0900
+++ b/paper/src/AgdaModusPonens.agda	Mon Feb 13 15:00:06 2017 +0900
@@ -1,2 +1,2 @@
-f : {A B C : Set} -> (A -> B) × (B -> C) -> (A -> C)
-f = (\p x -> snd p ((fst p) x))
+f : {A B C : Set} -> ((A -> B) × (B -> C)) -> (A -> C)
+f = \p x -> (snd p) ((fst p) x)
diff -r a133c32db45e -r 4e30a8a7128c paper/src/assert.c
--- a/paper/src/assert.c	Mon Feb 13 14:59:25 2017 +0900
+++ b/paper/src/assert.c	Mon Feb 13 15:00:06 2017 +0900
@@ -1,4 +1,4 @@
 void verifySpecification(struct Context* context, struct Tree* tree) {
     assert(!(maxHeight(tree->root, 1) > 2*minHeight(tree->root, 1)));
-    return meta(context, EnumerateInputs);
+    goto meta(context, EnumerateInputs);
 }