--- a/paper/agda.tex	Tue Jan 31 16:41:36 2017 +0900
+++ b/paper/agda.tex	Tue Jan 31 17:20:04 2017 +0900
@@ -412,8 +412,25 @@
 
 \lstinputlisting[label=src:agda-elem-apply, caption=部分型を持つ関数の適用] {src/AgdaElemApply.agda.replaced}
 
+最後にモジュールについて述べる。
+モジュールはほとんど名前空間として作用する。
+なお、依存型の解決はモジュールのインポート時に行なわれる。
+モジュールをインポートする時は \verb/import/ キーワードを指定する。
+また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。
+モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードを、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠す場合は \verb/hiding/ キーワードを用いる。
+なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open/ キーワードを使うことで展開できる。
+モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。
 
-% TODO: 必要なら with の解説
+\lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda}
+
+また、モジュールには値を渡すことができる。
+そのようなモジュールは Parameterized Module と呼ばれ、渡された値はそのモジュール内部で一貫して扱える。
+例えば要素の型と比較する二項演算子を使って並べ替えをするモジュール\verb/Sort/ を考える。
+そのモジュールは引数に型Aと二項演算子 \verb/</を取り、ソートする関数を提供する。
+\verb/Sort/モジュールを \verb/Nat/ と \verb/Bool/ で利用した例がリスト~\ref{src:agda-parameterized-module}である。
+
+\lstinputlisting[label=src:agda-parameterized-module, caption=Agda における Parameterized Module] {src/AgdaParameterizedModule.agda}
+
 
 \section{Reasoning}