Mercurial > hg > Papers > 2018 > nozomi-master
changeset 112:4e30a8a7128c
Merge
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 13 Feb 2017 15:00:06 +0900 |
| parents | a133c32db45e (current diff) 5ad74fb83f72 (diff) |
| children | 2e30ed0e2633 |
| files | paper/atton-master.pdf |
| diffstat | 4 files changed, 5 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- 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 で証明する。
--- 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)
--- 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); }