Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/abstract_eng.tex @ 82:39a27b704f0c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 08 Feb 2017 17:39:12 +0900
parents a92ac75bd9fa
children
comparison
equal deleted inserted replaced
81:3f63f697ed3a 82:39a27b704f0c
7 We checked red-black tree specification using our meta computation library named Akasha, which override program executions exhaustively. 7 We checked red-black tree specification using our meta computation library named Akasha, which override program executions exhaustively.
8 8
9 On the other hand method veriy programs with proofs. 9 On the other hand method veriy programs with proofs.
10 Proposition and proofs have isomorphic relation to typed $\lambda$ calculus by Curry-Howard Isomorphism. 10 Proposition and proofs have isomorphic relation to typed $\lambda$ calculus by Curry-Howard Isomorphism.
11 We define the CbC type system with subtype for proving CbC itself. 11 We define the CbC type system with subtype for proving CbC itself.
12 Agda proves properties of translated CbC programs using proposed subtype definition. 12 Dependent-typed language Agda proves properties of translated CbC programs using proposed subtype definition.
13 \end{abstract_eng} 13 \end{abstract_eng}