Mercurial > hg > Papers > 2017 > atton-master

changeset 110:5ad74fb83f72

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix
author atton
date Mon, 13 Feb 2017 14:18:03 +0900
parents f6d00a13f923
children 4e30a8a7128c
files paper/atton-master.pdf paper/cbc-type.tex
diffstat 2 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
Binary file paper/atton-master.pdf has changed
--- a/paper/cbc-type.tex	Mon Feb 13 14:11:30 2017 +0900
+++ b/paper/cbc-type.tex	Mon Feb 13 14:18:03 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 で証明する。