equal
deleted
inserted
replaced
72 \author{Cezary Kaliszyk} |
72 \author{Cezary Kaliszyk} |
73 \address{University of Tsukuba, Japan} |
73 \address{University of Tsukuba, Japan} |
74 \email{kaliszyk@score.cs.tsukuba.ac.jp} |
74 \email{kaliszyk@score.cs.tsukuba.ac.jp} |
75 |
75 |
76 \keywords{Nominal Isabelle, variable convention, formal reasoning} |
76 \keywords{Nominal Isabelle, variable convention, formal reasoning} |
77 \subjclass{MANDATORY list of acm classifications} |
77 \subjclass{F.3.1} |
78 |
78 |
79 \begin{abstract} |
79 \begin{abstract} |
80 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
80 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
81 prover. It provides a proving infrastructure for reasoning about |
81 prover. It provides a proving infrastructure for reasoning about |
82 programming language calculi involving named bound variables (as |
82 programming language calculi involving named bound variables (as |