nominal2: Paper/document/root.tex@7c607df46a0a (annotated)

1485 c004e7448dca temporarily disabled tests in Nominal/ROOT Christian Urban <urbanc@in.tum.de> parents: 1484 diff changeset	1	\documentclass{acmconf}
1493 52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	2	\usepackage{isabelle}
52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	3	\usepackage{isabellesym}
52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	4	\usepackage{amsmath}
52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	5	\usepackage{amssymb}
1506 7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	6	\usepackage{tikz}
7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	7	\usepackage{pgf}
7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	8	\usepackage{pdfsetup}
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	\urlstyle{rm}
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	\isabellestyle{it}
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	12
1493 52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	13	\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	14	\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	15	\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	16	\renewcommand{\isasymequiv}{$\dn$}
52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	17	\renewcommand{\isasymiota}{}
52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	18	\renewcommand{\isasymemptyset}{$\varnothing$}
52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	19
52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	20
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	21
1328 531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	22	%----------------- theorem definitions ----------
1506 7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	23	\newtheorem{Property}{Theorem}[section]
1328 531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	24	\newtheorem{Theorem}{Theorem}[section]
531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	25	\newtheorem{Definition}[Theorem]{Definition}
531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	26	\newtheorem{Example}{\it Example}[section]
531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	27
531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	28	%-------------------- environment definitions -----------------
531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	29	\newenvironment{example}[0]{\begin{Example} \it}{\end{Example}}
531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	30	\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	31
1485 c004e7448dca temporarily disabled tests in Nominal/ROOT Christian Urban <urbanc@in.tum.de> parents: 1484 diff changeset	32
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	\begin{document}
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	34
1493 52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	35	\title{\LARGE\bf General Binding Structures in Nominal Isabelle,\\ or How to
1328 531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	36	Formalise Core-Haskell}
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	\maketitle
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	38
1328 531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	39	\maketitle
531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	40	\begin{abstract}
1485 c004e7448dca temporarily disabled tests in Nominal/ROOT Christian Urban <urbanc@in.tum.de> parents: 1484 diff changeset	41	Nominal Isabelle is a definitional extension of the Isabelle/HOL
1506 7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	42	theorem prover. It provides a proving infrastructure for
7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	43	conveninet reasoning about programming language calculi. In this paper
7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	44	we present an extension of Nominal Isabelle for dealing with general binding
7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	45	structures. Such structures are ubiquitous in programming language research
7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	46	and only very poorly handled by the well-known single abstraction in the
7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	47	lambda-calculus. We give definitions for alpha-equivalence and establish
7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	48	the reasoning structure for alpha-equated terms. For example we provide
7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	49	a strong induction principle that has the variable convention already
7c607df46a0a slightly more in the paper Christian Urban <urbanc@in.tum.de> parents: 1493 diff changeset	50	built in.
1328 531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	51	\end{abstract}
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	52
1493 52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	53
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	54	\input{session}
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	55
1493 52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	56	\bibliographystyle{plain}
52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	57	\bibliography{root}
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	58
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	59	\end{document}
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	60
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	61	%%% Local Variables:
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	62	%%% mode: latex
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	63	%%% TeX-master: t
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	64	%%% End:

author	Christian Urban <urbanc@in.tum.de>
	Thu, 18 Mar 2010 11:33:37 +0100
changeset 1506	7c607df46a0a
parent 1493	52f68b524fd2
child 1517	62d6f7acc110
permissions	-rw-r--r--