<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
\documentclass[preprint]{drl-common/sigplanconf}
\usepackage{color}
\usepackage{stmaryrd}
\usepackage{arydshln}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{drl-common/proof}
\usepackage{drl-common/typesit,drl-common/typescommon}
\usepackage{drl-common/fancyvrb}
\usepackage{drl-common/code}
\usepackage[sort,round]{natbib}
\usepackage{wasysym} 
\usepackage{graphics}

\usepackage{ifthen}
\newboolean{tr}
\setboolean{tr}{false}

\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage[T1]{fontenc}

\usepackage{multicol}
\usepackage{fancyvrb}
\usepackage{drl-common/code}
\DefineVerbatimEnvironment{code}{Verbatim}{fontsize=\small,fontfamily=tt}

\newcommand{\ignore}[1]{}

%% small tightcode, with space around it
\newenvironment{stcode}
{\smallskip
\begin{small}
\begin{tightcode}}
{\end{tightcode}
\end{small}
\smallskip}

%% a marker to tell literate agda to ignore the code block
\newcommand{\noagda}[0]{}

\DeclareUnicodeCharacter{9001}{$\langle$}
\DeclareUnicodeCharacter{9002}{$\rangle$}
\DeclareUnicodeCharacter{12314}{$\llbracket$}
\DeclareUnicodeCharacter{12315}{$\rrbracket$}
\DeclareUnicodeCharacter{8872}{$\vDash$}
\DeclareUnicodeCharacter{9657}{$\triangleright$}
\DeclareUnicodeCharacter{9655}{$\triangleright$}
\DeclareUnicodeCharacter{8656}{$\Leftarrow$}
\DeclareUnicodeCharacter{0060}{$\Leftarrow$}
\DeclareUnicodeCharacter{8667}{\ensuremath{_\Rightarrow}}

\newcommand\textPsi{\ensuremath{\Psi}}
\newcommand\textXi{$\Xi$}
\newcommand\textDelta{$\Delta$}
\newcommand\textGamma{$\Gamma$}
\newcommand\textsigma{$\sigma$}
\newcommand\textSigma{$\Sigma$}
\newcommand\textPi{$\Pi$}
\newcommand\textrho{$\rho$}
\newcommand\textphi{$\varphi$}
\newcommand\textlambda{$\lambda$}
\newcommand\texttau{$\tau$}
\newcommand\texteta{$\eta$}
\newcommand\textmu{$\mu$}
\newcommand\textalpha{$\alpha$}
\newcommand\textepsilon{$\epsilon$}
\newcommand\textkappa{$\kappa$}
\newcommand\textOmega{$\Omega$}
\newcommand\textmho{$\mho$}
\newcommand\textgamma{$\gamma$}
\newcommand\textpi{$\varpi$}
\newcommand\textbeta{\ensuremath{\beta}}
\newcommand\textpsi{\ensuremath{\psi}}

\input{macros}

%% ----------------------------------------------------------------------
%% short names

\newcommand{\omegal}[0]{$\Omega$mega\/}
\newcommand{\FIXME}[1]{\textbf{FIXME:} #1}
\newcommand{\ttt}[1]{\texttt{#1}}

%% ----------------------------------------------------------------------

\begin{document}

\conferenceinfo{ICFP '09}{August, Edinburgh, Scotland} 
\copyrightyear{2009} 
%% \copyrightdata{[to be supplied]} 

\titlebanner{Submitted to ICFP '09}        % These are ignored unless

%% \conferenceinfo{PLPV'09,} {January 20, 2009, Savannah, Georgia, USA.}
%% \CopyrightYear{2009}
%% \copyrightdata{978-1-60558-330-3/09/01} 

\title{A Universe of Binding and Computation}
\subtitle{}

\authorinfo{Daniel R. Licata \and Robert Harper
%% FIXME: rename
%% \thanks{%
%% This research was sponsored in part by the National Science
%% Foundation under grant number CCF-0702381 and by the Carnegie Mellon
%% Anonymous Fellowship in Computer Science. The views and conclusions
%% contained in this document are those of the author and should not be
%% interpreted as representing the official policies, either expressed or
%% implied, of any sponsoring institution, the U.S. government or any other
%% entity.}
}
{Carnegie Mellon University}
{\texttt{\{drl,rwh\}@cs.cmu.edu}}

\maketitle

\begin{abstract}
In this paper, we construct a logical framework supporting datatypes
that mix binding and computation, implemented as a universe in the
dependently typed programming language Agda 2.  We represent binding
pronominally, using well-scoped de Bruijn indices, so types can be used
to reason about the scoping of variables.  We equip our universe with
datatype-generic implementations of weakening, substitution, exchange,
contraction, and subordination-based strengthening, so that programmers
are provided these operations for free for each language they define.
In our mixed, pronominal setting, weakening and substitution hold only
under some conditions on types, but we show that these conditions can be
discharged automatically in many cases.  Finally, we program a variety
of standard difficult test cases from the literature, such as
normalization-by-evaluation for the untyped $\lambda$-calculus,
demonstrating that we can express detailed invariants about variable
usage in a program's type while still writing clean and clear code.
\end{abstract}

%% \category{F.3.3}{Logics and Meanings Of Programs}{Studies of Program Constructs}[Type structure]
%% \category{F.3.1}{Logics and Meanings Of Programs}{Specifying and Verifying and Reasoning about Programs}[]
%% % \category{F.4.1}{Mathematical Logic And Formal Languages}{Mathematical Logic} [Proof theory, Lambda calculus and related systems]

%% \terms
%% Languages, Verification

\input{intro}
\input{defs}
\input{examples}
\input{structural}
\input{related}
\input{discussion}


\subsection*{Acknowledgements}  We thank Noam Zeilberger for discussions
about this work.

{\small
\bibliographystyle{abbrvnat}
{
\bibliography{drl-common/cs}
}}

\appendix

\input{bootcamp.lagda}


\end{document}