\documentclass[landscape]{slides}
\usepackage{latexsym}
% \usepackage{amssymb}
%\usepackage{cdsty}
\usepackage{fslide-com}
\usepackage{amsfonts}

\begin{document}
 \begin{slide}{}
  \vspace*{2em}
  \begin{center}
  {\bf Logical Frameworks} \\[1em]
  Tutorial at CADE-12 \\[1ex]
  Frank Pfenning\\
  Department of Computer Science\\
  Carnegie Mellon University \\[3em]
  For notes (in preparation) contact \\
  fp@cs.cmu.edu
  \end{center}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Overview}
 \begin{enumerate}
  \item Introduction
  \item Syntax
  \item Deductions
  \item Meta-programming and search
  \item Meta-theory
  \item Conclusion
 \end{enumerate}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Deductive Systems}
   {\bf Deductive systems} are a common conceptual tool in mathematical
logic and computer science.  They are used to specify, for example,
  \begin{itemize}
   \item Logics
   \item Type theories
   \item Type systems of programming languages
   \item Operational semantics 
   \item Compilation
   \item Algorithms (e.g. type inference, unification, theorem proving)
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Logical Frameworks}
  A {\bf logical framework} is a meta-language for the specification of
deductive systems.  Applications as a teaching and research tool include
  \begin{itemize}
   \item Reasoning {\bf within} a specified logic
   \item Implementation of algorithms (evaluation, type inference)
   \item Reasoning {\bf about\/} a deductive system
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Brief History, I}
  \begin{itemize}
   \item Automath [de Bruijn'68]
   \item Theory of Judgments [Martin-L\"of'85]
   \item (Edinburgh) Logical Framework \\ \relax
    [Harper, Honsell \& Plotkin'87] \\
    Elf [Pf'89,Pf'91]
   \item Hereditary Harrop Formulas \\ \relax
    [Nadathur, Miller, \& Scedrov'87] [Paulson'87] \\
    $\lambda$Prolog [Nadathur \& Miller'88] \\
    Isabelle [Paulson'89]
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Brief History, II}
 \begin{itemize}
  \item Inductive definitions / FS0 [Feferman'87]
  \item Inductive type theory / ALF [Coquand, Magnusson, Nordstr\"om'91]
  \item Partial inductive definitions/Pi [Halln\"as'87] [Eriksson'93]
  \item Labelled deductive systems [Gabbay'89]
  \item Substructural frameworks [Schroeder-Heister'91] [Girard'93] [Miller'94]
  \item Equational frameworks [Mart\`{\i}-Oliet \& Meseguer'93] [C.~Kirchner,
H.~Kirchner \& Vittek'93]
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Brief History, III}
 General systems for constructive mathematics have also been used
as logical frameworks.  For example:
  \begin{itemize}
   \item NQTHM (Boyer-Moore) [Shankar'86]
   \item Otter (Lusk-Overbeek) [Wos'88]
   \item Nuprl (Constable et al.) \\ \relax [Basin \& Constable'91]
   \item Coq (Huet et al.) [Huet'93]
   \item LEGO [Pollack'93]
  \end{itemize}
  \vfill
 \end{slide}



 \begin{slide}{}
  \slidetitle{Frameworks as Conceptual Tool}
  Logical frameworks, their concepts and methods can be an aid to
understanding, rather than just an implementation and checking device.
  \begin{itemize} \itemsep 0pt
   \item Polymorphic type reconstruction [Pf'88]
   \item Canonical forms and uniform derivations [Pf'92]
   \item Properties of CPS [Danvy \& Pf'93]
   \item Structural cut-elimination [Pf'94]
   \item Inductive residual theory [Huet'93]
   \item IsaWhelk [Basin'93]
   \item (Computation \& Deduction course [Pf'92,Pf'94])
   \item $\ldots$
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Framework Design Goals}
 \begin{itemize} \itemsep 0pt
  \item Simple and uniform, concise
  \item Close to (good) informal practice
  \item Efficiently implementable
  \item Support for search and meta-programming
  \item Decide validity of derivations
  \item Feasibility of proving correctness of representations
  \item Means for structuring large specifications
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Outline}
  Example: first-order predicate logic
  \begin{itemize}
   \item Abstract syntax
   \item Inference rules and derivations
   \item Search and meta-programming
   \item Meta-theory
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{FOL, Abstract Syntax}
 \[ \begin{array}{lrcl}
  \mbox{\it Variables} & x_n \\
  \mbox{\it Terms} & t & \bnfas & x \bnfalt f^k(t_1,\ldots,t_n) \\
  \mbox{\it Atoms} & P & \bnfas & p^k(t_1,\ldots,t_n) \\
  \mbox{\it Formulas} & A & \bnfas & P \bnfalt A_1 \limplies A_2 \bnfalt
\lnot A \bnfalt \forall x\ldot A 
 \end{array} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Uni-Typed Representation}
  Meta-Terms: First-order terms
  \[ \begin{array}{rcl}
  \rep{x_n} & = & \lf{var}(n) \\
  \rep{f^k(t_1,\ldots,t_n)} & = & \lf{c}_f^k(\rep{t_1},\ldots,\rep{t_n})
\\
  \rep{p^k(t_1,\ldots,t_n)} & = & \lf{c}_p^k(\rep{t_1},\ldots,\rep{t_n})
\\
  \rep{A \limplies B} & = & \lf{imp}(\rep{A},\rep{B}) \\
  \rep{\lnot A} & = & \lf{not}(\rep{A}) \\
  \rep{\forall x\ldot A} & = & \lf{forall}(\rep{x},\rep{A})
 \end{array} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{External Validity}
  Meta-Logic: Horn clauses
    \[ \begin{array}{rcl}
 D & \bnfas & \top \bnfalt D_1 \land D_2 \bnfalt P_1\land\ldots\land P_n
\limplies P \bnfalt \forall x\ldot D
 \end{array} \]
   Judgment: $\vdhorn D$
 \begin{lfsig}
  \lf{nat}(\lf{z}) \\
  \forall n\ldot \lf{nat}(n) \limplies \lf{nat}(\lf{s}(n)) \\[1em]
  \forall n\ldot \lf{nat}(n) \limplies \lf{variable}(\lf{var}(n)) \\[1em]
  \forall t\ldot \lf{variable}(t) \limplies \lf{term}(t) \\[1em]
  \forall A\ldot \forall B\ldot \lf{formula}(A) \land \lf{formula}(B) \\
\qquad \null \limplies \lf{formula}(\lf{and}(A,B)) \\
  \forall A\ldot \lf{formula(A)} \limplies \lf{formula}(\lf{not}(A)) \\
  \forall x\ldot \forall A\ldot \lf{variable}(x) \land \lf{formula}(A) \\
\qquad \null \limplies \lf{formula}(\lf{forall}(x,A))
 \end{lfsig}%
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Representation Theorem}
 {\bf Theorem} (Representation)
 \begin{enumerate} \itemsep 0pt
   \item $F \vdhorn \lf{variable}(t')$ iff $t' = \rep{x}$ for a variable $x$.
   \item $F \vdhorn \lf{term}(t')$ iff $t' = \rep{t}$ for a term $t$.
   \item $F \vdhorn \lf{formula}(t')$ iff $t' = \rep{A}$ for a formula $A$.
 \end{enumerate}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Assessment}
 Problems:
 \begin{itemize} \itemsep 0pt
  \item External validity
  \item Does not capture ``variable convention'', renaming
  \item Awkward substitution and meta-theory
 \end{itemize}

 Solutions: 
 \begin{itemize} \itemsep 0pt
  \item Internal validity via typing
  \item de Bruijn indices or higher-order abstract syntax 
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Simply-Typed Representation}
   Meta-terms: simply-typed $\lambda$-terms
   \begin{itemize} \itemsep 0pt
    \item Internal validity as typing
    \item Higher-order abstract syntax: \\ 
          Object variables as meta-language variables
   \end{itemize}
 System $\lambda^\arrow$
 \[ \begin{array}{lrcl}
  \mbox{Types} & A & \bnfas & a \bnfalt A_1 \arrow A_2 \\
  \mbox{Objects} & M & \bnfas & c \bnfalt x \bnfalt \lam x\oftp A\ldot M
\bnfalt M_1\; M_2 \\[1ex]
  \mbox{Signatures} & \Sigma & \bnfas & \cdot \bnfalt \Sigma, a\oftp\type
\bnfalt \Sigma, c\oftp A \\
  \mbox{Contexts} & \Gamma & \bnfas & \cdot \bnfalt \Gamma, x\oftp A
 \end{array} \]
 \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Judgments of $\lambda^\arrow$}
 Static
  \[ \begin{array}{ll}
  \vdlf A \hastype \type & \mbox{$A$ is a valid type} \\
  \gvdlf M \hastype A & \mbox{$M$ is a valid object of type $A$} \\
  \vdlf \Sigma\; \isasig & \mbox{$\Sigma$ is a valid signature} \\
  \vdlf \Gamma\; \isactx & \mbox{$\Gamma$ is a valid context} \\
  \gvd M \canon A & \mbox{$M$ is canonical of type $A$} \\
  \gvd M \atm A & \mbox{$M$ is atomic of type $A$} \\
 \end{array} \]

 Dynamic
  \[ \begin{array}{cl}
 M \whr M' & \mbox{$M$ weakly head reduces to $M'$} \\
 \gvd M \can M' \hastype A & \mbox{$M$ has canonical form $M'$} \\
 \gvd M \atm M' \hastype A & \mbox{$M$ has atomic form $M'$}
 \end{array} \]

 Note: will omit signature $\Sigma$
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{$\lambda^\arrow$ Typing}
 
 \[ \rulespacing \begin{array}{c}
  \ian{\Sigma(c) = A}{\gvdlf c \hastype A}{\cf con} \hspace{5em}
  \ian{\Gamma(x) = A}{\gvdlf x \hastype A}{\cf var} \\
  \ibn{\vdlf A \hastype \type}{\Gamma, x\oftp A \vdlf M \hastype B}{\gvdlf
\lam x\oftp A\ldot M \hastype A \arrow B}{\cf lam} \\
  \ibn{\gvdlf M \hastype A \arrow B}{\gvdlf N \hastype A}{\gvdlf M\; N
\hastype B}{\cf app}
  \end{array} \] 

  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{$\lambda^\arrow$ Canonical Forms}
 {\bf Canonical forms} play the role of observable values in functional
languages.  They can also be defined as long $\beta\eta$-normal forms.
 \[ \rulespacing \begin{array}{c}
 \ian{\Gamma, x\oftp A \vd M \can B}{\gvd \lam x\oftp A\ldot M \can A \arrow
B}{{\cf can\_lam}} \\
 \ianc{\gvd M \atm a}{\gvd M \can a}{{\cf can\_atm}} \\
 \ian{\Gamma(x) = A}{\gvd x \atm A}{{\cf atm\_var}} \\
 \ian{\Sigma(c) = A}{\gvd c \atm A}{{\cf atm\_con}} \\
 \ibn{\gvd M \atm B \arrow A}{\gvd N \can B}{\gvd M\, N \atm A}{{\cf
atm\_app}}
 \end{array} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Some Properties}
 {\bf Theorem} (Properties of $\lambda^\arrow$)
 \begin{enumerate} \itemsep 0pt
  \item All judgments are decidable.
  \item Every term has a unique canonical form.
  \item $\beta\eta$-conversion are admissible rules for definitional equality.
 \end{enumerate}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Simply-Typed Representation}
   \[ \begin{tabular}{|c|c|} \hline
   Syntactic category & Atomic type \\ \hline
   Expressions & Canonical forms \\ \hline
   \end{tabular} \]
  \begin{lfsig}
  \lfi & \hastype & \type \\
 \end{lfsig}%
 \[ \begin{array}{rcl}
  \rep{x} & = & x \\
  \rep{f(t_1,\ldots,t_n)} & = & \lf{f}\; \rep{t_1}\ldots \rep{t_n} \\
  \lf{f} & \hastype & \lfi \arrow \cdots \arrow \lfi
 \end{array} \]
 \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Representing Formulas}
  \begin{lfsig}
   \lfo & \hastype & \type
  \end{lfsig}%
 \[ \begin{array}{rcl@{\hspace{3em}}lcl}
  \rep{P(t_1,\ldots,t_n)} & = & \lf{p}\; \rep{t_1}\ldots \rep{t_n} \\
  \lf{p} & \hastype & \lfi \arrow \cdots \arrow \lfo \\[1ex]
  \rep{A_1 \limplies A_2} & = & \lf{imp}\; \rep{A_1}\; \rep{A_2} \\
  \lf{imp} & \hastype & \lfo \arrow \lfo \arrow \lfo \\[1ex]
  \rep{\lnot A} & = & \lf{not}\; \rep{A} \\
  \lf{not} & \hastype & \lfo \arrow \lfo \\[1ex]
  \rep{\forall x\ldot A} & = & \lf{forall}\; (\lam x\oftp\lfi\ldot \rep{A}) \\
\lf{forall} & \hastype & (\lfi \arrow \lfo) \arrow \lfo
 \end{array} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Higher-Order Abstract Syntax}
   \[ \begin{tabular}{|c|c|} \hline
    Object Lang & Meta-Lang \\ \hline \hline
    Variable & Variable \\ \hline
    Binding Construct & Second-Order Constant \\
    $\rep{\forall x\ldot A}$ & $\lf{forall}\, (\lam x\oftp\lfi\ldot \rep{A})$
\\ \hline
    Renaming & $\alpha$-Conversion \\ \hline
    Substitution & $\beta$-Reduction \\ \relax
    $[t/x] A$ & $\rep{[t/x]A} = [\rep{t}/x]\rep{A}$ \\
            & $\equiv (\lam x\oftp\lfi \ldot \rep{A})\, \rep{t}$ \\ \hline
   \end{tabular} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Representation Theorem}
  {\bf Theorem} (Representation)
  \begin{enumerate}
   \item $x_1\oftp \lfi,\ldots,x_n\oftp \lfi \vdlf M \can \lfi
\quad\mbox{iff}\quad M = \rep{t}$
  where the free variables of $t$ are among $x_1,\ldots,x_n$.
  \item $x_1\oftp \lfi,\ldots,x_n\oftp \lfi \vdlf M \can \lfo
\quad\mbox{iff}\quad M = \rep{A}$
  where the free variables of $A$ are among $x_1,\ldots,x_n$.
 \item The representation function $\rep{\cdot}$ is {\bf compositional\/} in
the sense that
 \[ [\rep{t}/x]\rep{s} = \rep{[t/x]s}\]
and
  \[ [\rep{t}/x]\rep{A} = \rep{[t/x]A} \]
  \end{enumerate}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Why Canonical Forms}
 Assume $p \oftp \lfi \arrow \lfo$.  Then
 \[ \begin{array}{c}
   \lf{forall}\, (\lam x\oftp\lfi \ldot ((\lam q\oftp\lfo\ldot q)\, (p\, x)))
\hastype \lfo \\
   \lf{forall}\, p \hastype \lfo 
 \end{array} \]
 are not in the image of the representation function $\rep{\cdot}$.
Their canonical form
  \[ \begin{array}{c}
 \lf{forall}\, (\lam x\oftp\lfi\ldot p\, x) \tocan \lfo
 \end{array} \]
 is.
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Summary: Syntax}
   \begin{itemize} \itemsep 0pt
    \item Uni-typed vs simply-typed representation
    \item External vs internal validity
    \item Variables as constants, de Bruijn indices, or meta-variables
    \item Higher-order abstract syntax:
    \begin{itemize}
     \item Expressions $\Longrightarrow$ canonical forms
     \item Renaming $\Longrightarrow$ $\alpha$-conversion
     \item Substitution $\Longrightarrow$ $\beta$-reduction
    \end{itemize}
    \item Inductive vs open-ended representation
   \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Representing Deductions}
   \begin{itemize} \itemsep 0pt
    \item Derivability vs deductions-as-objects
    \item External vs internal validity
    \item Inductive vs open-ended representation
   \end{itemize}

   Styles of deductive systems
   \begin{itemize} \itemsep 0pt
    \item Axiomatic [Hilbert'17]
    \item Natural Deduction [Gentzen'35]
    \item Sequents [Gentzen'35]
   \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Judgments}
  \begin{itemize} \itemsep 0pt
   \item A {\bf judgment} is defined (inductively) by inference rules
   \item Axiom = inference rule with no premisses
   \item Hypothetical judgment
 \[ \hypol{\ian{}{J_1}{u}}{\vdots}{J_2} \]
 Judgment $J_2$ is derivable under hypothesis $J_1$ labelled $u$.
Salient properties: substitution, exchange, duplication, weakening.
   \item Parametric judgment.  Salient property: substitution.
   \item Discharge of hypotheses or parameters indicated by superscript
on inference.
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Natural Deduction}
  Judgment $\vdnd A$

  Each connective is characterized by introduction and elimination rules,
which must match up in the form of a (local) reduction.

  Higher-level judgment
 \[ \above{\DD}{\vdnd A} \ndredl \above{\DD'}{\vdnd A} \]

  Note: we will drop the turnstile ($\vdnd$).
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{ND/Implication}
 \[ \ianc{\hypo{\ian{}{A}{u}}{B}}{A \limplies B}{\impi^u} \]

 \[ \ibnc{A \limplies B}{A}{B}{\impe} \]

 \[ \ctr{\ianc{\ian{\hypol{\ian{}{A}{u}}{\DD}{B}}{A \limplies
B}{\impi^u} \hspace{4em} \above{\EE}{A}}{B}{\impe} }
 \ndredl
  \hypolc{\ian{\EE}{A}{u}}{\DD}{B} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{ND/Negation}
  Typically: $\lnot A = A \limplies \bot$.  Instead, we use a judgment
{\bf parametric} in a formula $p$.
 \[ \ianc{\hypo{\ian{}{A}{u}}{p}}{\lnot A}{\noti^{u,p}} \hspace{5em}
 \ibnc{\lnot A}{A}{C}{\note} \]

 \[ \ctr{\ianc{\ian{\hypol{\ian{}{A}{u}}{\DD}{p}}{\lnot A}{\noti^{u,p}}
\hspace{4em} \above{\EE}{A}}{C}{\note} }
 \ndredl
  \hypolc{\ian{\EE}{A}{u}}{{[C/p]}\DD}{C} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{ND/Universal Quantification}
  \[ \ianc{[a/x]A}{\forall x\ldot A}{\foralli^a} \hspace{5em}
  \ianc{\forall x\ldot A}{[t/x]A}{\foralle} \]
 where the premiss of $\foralli^a$ is parametric in $a$.

 \[ \ctr{\ianc{\ian{\above{\DD}{[a/x]A}}{\forall x\ldot
A}{\foralli^a}}{[t/x]A}{\foralle}}
 \ndredl
 \abovec{[t/a]\DD}{[t/x]A} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{A Counterexample}
 \sbox{\tempdedA}{\ian{\ian{\ian{}{P(a)}{u}}{\forall x\ldot
P(x)}{\foralli^a\mbox{?}}}{P(b)}{\foralle}}
 \[ \ian{\ian{\ian{\usebox{\tempdedA}}{P(a) \limplies P(b)}{\impi^u}}{\forall
y\ldot P(a) \limplies P(y)}{\foralli^b}}{\forall x\ldot \forall y\ldot P(x)
\limplies P(y)}{\foralli^a} \]

would locally reduce to

 \[ \ian{\ian{\ian{\ian{}{P(b)}{u}}{P(a) \limplies
P(b)}{\impi^u\mbox{?}}}{\forall y\ldot P(a) \limplies
P(y)}{\foralli^b}}{\forall x\ldot \forall y\ldot P(x) \limplies
P(y)}{\foralli^a} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{ND/Classical Logic}
  Take, for example, one of
  \[ \ianc{\lnot \lnot A}{A}{\cf dbneg} \hspace{5em} \ianc{\hypo{\lnot
A}{A}}{A}{\cf contr} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{ND/An Example}
 \[ \begin{array}{ccc}
 \ctr{\hypoc{}{A \limplies \lnot \lnot A}}
 & \leadsto &
 \ctr{\ianc{\hypo{\ian{}{A}{u}}{\lnot \lnot A}}{A \limplies \lnot \lnot
A}{\impi^u}}
 \end{array} \]

\sbox{\tempdedA}{\ibn{\ian{}{\lnot A}{w}}{\ian{}{A}{u}}{p}{\note}}
\sbox{\tempdedB}{\hypo{\ian{}{A}{u}\hspace{2em} \ian{}{\lnot
A}{w}}{p}}
 \[ \begin{array}{cccc}
 \leadsto &
 \ctr{\ianc{\ian{\usebox{\tempdedB}}{\lnot \lnot A}{\noti^{w,p}}}{A
\limplies \lnot \lnot A}{\impi^u}}
 \leadsto \hspace{2em} &
 \ctr{\ianc{\ian{\usebox{\tempdedA}}{\lnot \lnot A}{\noti^{w,p}}}{A \limplies
\lnot \lnot A}{\impi^u}}
 \end{array} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Representing Derivability}
 [Paulson'86] [Felty \& Miller'88]
 \begin{itemize} \itemsep 0pt
  \item Meta-terms: simply-typed $\lambda$-terms
  \item Meta-logic: hereditary Harrop formulas
 \end{itemize}

{\bf Hereditary Harrop Formulas}
\[ \begin{array}{rcl}
  H & \bnfas & P \bnfalt \top \bnfalt H_1 \land H_2 \bnfalt H_1 \limplies H_2
\bnfalt \forall x\oftp A\ldot H \end{array} \]
  (Note: $A$ stands for simple types, $P$ for atomic formulas)

  Difference to Horn logic:
  \begin{itemize} \itemsep 0pt
    \item types
    \item embedded implication
    \item embedded universal quantification
   \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Derivability as a Predicate}
   Inference rules as axioms
 \begin{lfsig}
  \forall A\oftp\lfo\ldot \forall B\oftp\lfo \ldot (\lf{nd}\, (\lf{imp}\,
A\, B)\, \land \lf{nd}\, A) \limplies \lf{nd}\, B
 \end{lfsig}%

  Hypothetical judgments via embedded implication
 \begin{lfsig}
  \forall A\oftp\lfo \ldot \forall B\oftp\lfo \ldot (\lf{nd}\, A \limplies
\lf{nd}\, B) \limplies \lf{nd}\, (\lf{imp}\, A\, B)
 \end{lfsig}%

  Meta-logic must be weak, so that not too many propositions $\lf{nd}\, A$
are provable.
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Representation Theorem}
   Parametric judgments via embedded universal quantification (to be explained
later).  Complete theory ${\it ND}$
 \begin{lfsig}
  \forall A\oftp \lfo \ldot (\forall p\oftp \lfo\ldot \lf{nd} (A) \limplies
\lf{nd}(p)) \limplies \lf{nd}(\lnot A) \\
  \forall A\oftp \lfo \ldot \lf{nd}(\lnot A) \limplies \forall C\oftp\lfo\ldot
(\lf{nd}(A) \limplies \lf{nd}(C)) \\
  \forall A\oftp \lfi \arrow \lfo\ldot (\forall x\oftp\lfi\ldot \lf{nd}\, (A\,
x)) \\
 \qquad \null \limplies \lf{nd}\, (\lf{forall}\, (\lam x\oftp\lfi\ldot A\, x))
\\
  \forall A\oftp\lfi \arrow \lfo \ldot \lf{nd}\, (\lf{forall}\, (\lam
x\oftp\lfi\ldot A\, x)) \\
 \qquad \null \limplies (\forall x\oftp\lfi\ldot \lf{nd}\, (A\, x))
 \end{lfsig}%

  {\bf Theorem} (Representation)
    \[ {\it ND} \vdhhf \lf{nd}(\rep{A}) \quad\mbox{iff}\quad \vdnd A \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Deductions as Objects}
   Useful in many circumstances
   \begin{itemize} \itemsep 0pt
    \item Proof transformation (local reduction)
    \item Program extraction
    \item Metatheory (normalization, logical interpretations)
   \end{itemize}

   Try: simply-typed $\lambda$-calculus
   \begin{itemize} \itemsep 0pt
    \item Introduce {\bf type} $\lf{nd}$ of natural deductions
    \item Example: $\lf{impe} \hastype \lfnd \arrow \lfnd \arrow \lfnd$
    \item Requires external validity
    \item Not {\em a priori} decidable
   \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Type Families}
 First attempt:
 \begin{lfsig}
  \lf{impe} & \hastype & \lfnd\, (\lf{imp}\, A\, B) \arrow \lfnd\, A \arrow
\lfnd\, B
 \end{lfsig}%
  Here, $\lfnd$ is a {\bf type family} indexed by objects of type $\lfo$.
 \begin{lfsig}
  \lfnd & \hastype & \lfo \arrow \type
 \end{lfsig}%
  Declaration is schematic in $A$ and $B$.  Allowing such declarations
leads to an undecidable type-checking problem [Dowek'93].
 \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Dependent Function Types}
  Solution: add $A$ and $B$ are arguments to $\lf{impe}$.  However,
  \begin{lfsig}
  \lf{impe} & \hastype & \lfo \arrow \lfo \arrow \lfnd\, (\lf{imp}\, A\, B)
\arrow \lfnd\, A \arrow \lfnd\, B
 \end{lfsig}%
  loses information on argument dependence.

  Solution: name the argument via the {\bf dependent function type constructor}
$\Pi$.
 \begin{lfsig}
  \lf{impe} & \hastype & \Pi A\oftp\lfo\ldot \Pi B\oftp\lfo\ldot\\
 & & \quad \lfnd\, (\lf{imp}\, A\, B) \arrow \lfnd\, A \arrow \lfnd\, B
 \end{lfsig}%
 \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Dependent Typing Rules}
 \[ \begin{array}{c}
   \ibn{\gvdlf M \hastype \Pi x\oftp A\ldot B}{\gvdlf N \hastype A}{\gvdlf
M\; N \hastype [N/x]B}{\cf app}
 \end{array} \]

 For example:
 \[ \begin{array}{c}
  \lf{impe}\, (\lf{not}\, p)\, p \hastype \\
 \quad \lfnd\, (\lf{imp}\, (\lf{not}\, p)\, p)
\arrow \lfnd\, (\lf{not}\, p) \arrow \lfnd\, p
 \end{array} \]

 \[ \begin{array}{c}
   \ibn{\gvdlf A \hastype \type}{\Gamma, x\oftp A \vdlf M \hastype B}{\gvdlf
 \lam x\oftp A\ldot M \hastype \Pi x\oftp A\ldot B}{\cf lam}
 \end{array} \]

  These rule for $\Pi x\oftp A\ldot B$ specialize to $A \arrow B$ if $x$ does
not occur in $B$.
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Type Conversion I}
 Excursion into functional programming

 \begin{lfsig}
  \lf{concat} & \hastype & \Pi n\oftp\lf{nat}\ldot \Pi m\oftp\lf{nat}\ldot \\
 & & \quad \lf{vector}\, n \arrow \lf{vector}\, m \\
 & & \quad\arrow \lf{vector}\, (n+m)
 \end{lfsig}%
 Calculate:
 \begin{lfsig}
  \lf{concat}\, 2\, 3\, [1,2]\, [1,3,5] & \hastype & \lf{vector}(2+3) \\
  \lf{concat}\, 3\, 2\, [1,2,1]\, [3,5] & \hastype & \lf{vector}(3+2)
 \end{lfsig}%
 Both evaluate to
 \begin{lfsig}
  [1,2,1,3,5] & \hastype & \lf{vector}(5),
 \end{lfsig}%
 All should have the same type.

  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Type Conversion II}
 
 \[ \begin{array}{c}
  \ian{\gvdlf M \hastype A \hspace{3em} \gvdlf A \conv B \hastype
\type}{\gvdlf M \hastype B}{\cf conv}
 \end{array} \]

  \begin{itemize} \itemsep 0pt
   \item Typing depends on conversion
   \item Undecidable in a functional language due to {\em recursion}
   \item Decidable in framework: function spaces are intensional for
representation of binding, not for functional computation
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Summary, Dependent Types}
 Dependently typed $\lambda$-calculus $\lambda^\Pi$ \\ \relax
 (Edinburgh) LF [Harper, Honsell \& Plotkin'87,'93]
 \[ \begin{array}{lrcl}
  \mbox{Kinds} & K & \bnfas & \type \bnfalt \Pi x\oftp A\ldot K \\
  \mbox{Families} & A & \bnfas & a \bnfalt A\; M \bnfalt \Pi x\oftp A_1\ldot
A_2 \\
  \mbox{Objects} & M & \bnfas & c \bnfalt x \bnfalt \lam x\oftp A\ldot M
\bnfalt M_1\; M_2 \\[1ex]
  \mbox{Signatures} & \Sigma & \bnfas & \cdot \bnfalt \Sigma, a\oftp K
\bnfalt \Sigma, c\oftp A \\
  \mbox{Contexts} & \Gamma & \bnfas & \cdot \bnfalt \Gamma, x\oftp A
 \end{array} \]

 \begin{itemize} \itemsep 0pt
  \item Typing and canonical forms extend from $\lambda^\arrow$
  \item Type checking remains decidable \\ \relax
  [HHP'87] [Salvesen'90] [Coquand'91] [Geuvers'93] (in $\lambda$-cube)
  \item Every well-typed object has a canonical form
  \item Theory more difficult due to type conversion
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{ND in LF, Implication Intro}
 \[ \bigrep{\ianc{\hypol{\ian{}{A}{u}}{\DD}{B}}{A \limplies B}{\impi^u}} =
\lf{impi}\; \rep{A}\; \rep{B}\; (\lam u\oftp \lfnd\; \rep{A}\ldot \rep{\DD}) \]
 The hypothesis $A$ labelled by $u$ is represented by an LF variable $u$.
 \[ \bigrep{\ianc{}{A}{u}} = u \]
 Thus
 \begin{lfsig}
  \lf{impi} & \hastype & \Pi A \oftp \lfo\ldot \Pi B\oftp\lfo \ldot\\
 & & \quad (\lfnd\, A \arrow \lfnd\, B) \arrow \lfnd\, (\lf{imp}\, A\, B)
 \end{lfsig}%
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{ND in LF, Implication Elim}
 \[ \bigrep{\ibnc{\above{\DD}{A \limplies B}}{\above{\EE}{A}}{B}{\impe}} =
\lf{impe}\; \rep{A}\; \rep{B}\; \rep{\DD}\; \rep{\EE} \]
 where
 \begin{lfsig}
  \lf{impe} & \hastype & \Pi A\oftp \lfo \ldot \Pi B\oftp \lfo \ldot\\
 & & \quad \lfnd\; (\lf{imp}\; A\; B) \arrow \lfnd\; A \arrow \lfnd\; B.
 \end{lfsig}%
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{ND in LF, Example}
 \[ \ianc{\ian{\ian{}{A}{u}}{B \limplies A}{\impi^w}}{A \limplies (B
\limplies A)}{\impi^u} \]
 represented by the LF object
 \[ \begin{array}{l}
  \lf{impi}\; \repA\; (\lf{imp}\; \repB\; \repA) \\
 \quad (\lam u\oftp \lfnd\; \repA\ldot \lf{impi}\; \repB\; \repA\; (\lam
w\oftp \lfnd\; \repB\ldot u))
 \end{array} \]
 of type
 \[ \lfnd\; (\lf{imp}\; \repA\; (\lf{imp}\; \repB\; \repA)) \]

 (Note representational redundancies)
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{ND in LF, Negation Intro}
 \[ \bigrep{\ianc{\hypol{\ian{}{A}{u}}{\DD}{p}}{\lnot A}{\noti^{u,p}}} =
\lf{noti}\; \rep{A}\; (\lam p\oftp\lfo\ldot \lam u\oftp\lfnd\, \rep{A}\ldot
\rep{\DD}) \]
 The premiss is parametric in $p$.  This is represented as a function
from a $p$ and a deduction of $A$ to a deduction of $p$.
 \begin{lfsig}
  \lf{noti} & \hastype & \Pi A\oftp\lfo \ldot (\Pi p\oftp\lfo\ldot \lfnd\; A
\arrow \lfnd\; p) \\
 & & \quad \arrow \lfnd\; (\lf{not}\; A)
 \end{lfsig}%
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{ND in LF, Negation Elim}
 \[ \bigrep{\ibnc{\above{\DD}{\lnot A}}{\above{\EE}{A}}{C}{\note}} =
\lf{note}\; \rep{A}\; \rep{\DD}\; \rep{C}\; \rep{\EE} \]

 \begin{lfsig}
  \lf{note} & \hastype & \Pi A\oftp\lfo \ldot \lfnd\; (\lf{not}\; A) \\
 & & \quad \null \arrow \Pi C\oftp\lfo\ldot \lfnd\; A \arrow \lfnd\; C
 \end{lfsig}%
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{ND in LF, Universal Intro}
 Parametric judgment as a function
 \[ \bigrep{\ianc{\above{\DD}{[a/x]A}}{\forall x\ldot A}{\foralli^a}} =
\lf{foralli}\; (\lam x\oftp\lfi\ldot \rep{A})\; (\lam a\oftp\lfi \ldot
\rep{\DD}) \]

  \begin{lfsig}
  \lf{foralli} & \hastype & \Pi A\oftp \lfi \arrow \lfo\ldot (\Pi a\oftp \lfi
\ldot \lfnd\; (A\; a)) \\
 & & \quad \arrow \lfnd\; (\lf{forall}\; A)
 \end{lfsig}%
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{ND in LF, Universal Elim}
 Substitution via application and $\beta$-reduction
 \[ \bigrep{\ianc{\above{\DD}{\forall x\ldot A}}{[t/x]A}{\foralle}} =
\lf{foralle}\; (\lam x\oftp\lfi\ldot \rep{A})\; \rep{\DD}\; \rep{t} \]

 \begin{lfsig}
  \lf{foralle} & \hastype & \Pi A\oftp \lfi \arrow \lfo\ldot
\lfnd\; (\lf{forall}\; A) \\
 & & \quad \arrow \Pi t\oftp \lfi\ldot \lfnd\; (A\; t)
 \end{lfsig}%

  Check:
   \[ \bigrep{\ianc{\above{\DD}{\forall x\ldot A}}{[t/x]A}{\foralle}} \hastype
\lfnd\; \rep{[t/x] A}, \]
 assuming that $\rep{\DD} \hastype \lfnd\; \rep{\forall x\ldot A}$.
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Type Conversion III}
 \begin{small}
 \[ \begin{array}{l}
 \lf{foralle}  \hastype  \Pi A\oftp \lfi \arrow \lfo\ldot
\lfnd\; (\lf{forall}\; A) \arrow \Pi t\oftp \lfi\ldot \lfnd\; (A\; t) \\
 \lf{foralle}\; (\lam x\oftp\lfi\ldot \rep{A})  \hastype  \lfnd\;
(\lf{forall}\; (\lam x\oftp\lfi\ldot \rep{A})) \arrow \\
 \hspace{12em} \Pi t\oftp \lfi\ldot \lfnd\; ((\lam x\oftp\lfi\ldot \rep{A})\;
t) \\
 \lf{foralle}\; (\lam x\oftp\lfi\ldot \rep{A})\; \rep{\DD}  \hastype 
\Pi t\oftp \lfi\ldot \lfnd\; ((\lam x\oftp\lfi\ldot \rep{A})\; t) \\
 \lf{foralle}\; (\lam x\oftp\lfi\ldot \rep{A})\; \rep{\DD}\; \rep{t} 
\hastype  \lfnd\; ((\lam x\oftp\lfi \ldot \rep{A})\; \rep{t}) \\
 \lf{foralle}\; (\lam x\oftp\lfi\ldot \rep{A})\; \rep{\DD}\; \rep{t} 
\hastype  \lfnd\; ([\rep{t}/x]\rep{A}) \\
\lf{foralle}\; (\lam x\oftp\lfi\ldot \rep{A})\; \rep{\DD}\; \rep{t}
  \hastype  \lfnd\; (\rep{[t/x] A})
 \end{array} \]
 \end{small}

 Last two steps by type conversion and compositionality of $\rep{\cdot}$
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Representation Theorem}
  {\bf Theorem} (Representation)
  \begin{enumerate} \itemsep 0pt
   \item Let $\DD$ be derivation from hypotheses $A_1,\ldots, A_n$ labelled
$u_1,\ldots,u_n$ with free variables among $x_1, \ldots, x_m$.  Then
 \[ \begin{array}{l}
 x_1\oftp\lfi, \ldots, x_m\oftp\lfi, u_1\oftp\lfnd\, \rep{A_1}, \ldots,
u_n\oftp\lfnd\, \rep{A_n} \\
 \vdlf \rep{\DD} \can \lfnd\, \rep{A} 
 \end{array} \]
  \item If
 \[ \begin{array}{l} x_1\oftp\lfi, \ldots, x_m\oftp\lfi, u_1\oftp\lfnd\,
\rep{A_1}, \ldots, u_n\oftp\lfnd\, \rep{A_n} \\ \vdlf \rep{\DD} \can \lfnd\,
\rep{A} \end{array} \]
 then $M = \rep{\DD}$ as in part 1.
  \item The representation is compositional:
 \[ \begin{array}{rcl}
 \rep{[t/x]\DD} & = & [\rep{t}/x]\rep{\DD}\\
 \rep{[C/p]\DD} & = & [\rep{C}/p]\rep{\DD}\\
 \rep{[\EE/u]\DD} & = & [\rep{\EE}/u]\rep{\DD}
 \end{array} \]
  \end{enumerate}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{LF Implementation in Elf}
   Elf [Pf'89,Pf'91]
   \begin{itemize} \itemsep 0pt
    \item $\Pi x\oftp A\ldot B$ as \verb"{x:A} B"
    \item $\lam x\oftp A\ldot B$ as \verb"[x:A] B"
    \item \verb"B <- A" same as \verb"A -> B"
    \item Type and object reconstruction
    \item Undecidable (may answer yes, no, or maybe)
    \item Crucial in practice
    \item Duality: implicit $\Pi$-quantifier $\leftrightarrow$ implicit
argument
    \item Later: logic programming
   \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{FOL in Elf}
 %file elf/fol.elf
 \begin{verbatim}
tm : type.  % individuals
fo : type.  % formulas

imp    : fo -> fo -> fo.  %infix right 10 imp
not    : fo -> fo.        %prefix 12 not
forall : (tm -> fo) -> fo.

nd : fo -> type.  % deductions

impi    : (nd A -> nd B) -> nd (A imp B).
impe    : nd (A imp B) -> nd A -> nd B.

noti    : ({p:fo} nd A -> nd p) -> nd (not A).
note    : nd (not A) -> {C:fo} nd A -> nd C.

foralli : ({a:tm} nd (A a)) -> nd (forall A).
foralle : nd (forall A) -> {T:tm} nd (A T).

?- (impi [u:nd A] impi [w:nd B] u)
   : nd (A imp (B imp A)). \end{verbatim}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Summary: Deductions}
  \begin{itemize} \itemsep 0pt
   \item Derivability vs deductions-as-objects
   \item External vs internal validity
   \item ($\lambda^\arrow$+hhf) vs ($\lambda^\pi$) [Felty'90]
   \item $\lambda$Prolog, Isabelle vs Elf
   \item LF: Judgments-as-types
   \item Hypothetical judgments as functions
   \item Parametric judgments as functions
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Judgments Relating Derivations}
  Local Reduction
 \[ \abovec{\DD}{\vdnd A} \ndredl \abovec{\DD'}{\vdnd A} \]
  Represented as type family indexed by deductions.
   \begin{lfsig}
  \lf{redl} & \hastype & \Pi A\oftp\lfo \ldot \lfnd\; A \arrow \lfnd\; A
\arrow \type
  \end{lfsig}%

 \begin{verbatim}
==>L : nd A -> nd A -> type.
%infix none 14 ==>L \end{verbatim}

 Type checking guarantees the same conclusion
 
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Local Reduction, Implication}
 
 \[ \ctr{\ianc{\ian{\hypol{\ian{}{A}{u}}{\DD}{B}}{A \limplies
B}{\impi^u} \hspace{4em} \above{\EE}{A}}{B}{\impe} }
 \ndredl
  \hypolc{\ian{\EE}{A}{u}}{\DD}{B} \]
 Recall Compositionality:
 \[ \rep{[\EE/u]\DD} = [\rep{\EE}/u]\rep{\DD} \equiv (\lam u\oftp \lfnd\;
\rep{A}\ldot \rep{\DD})\; \rep{\EE} \]
 %file src/natded/red.elf
 \begin{verbatim}
redl_imp    : (impe (impi D) E) ==>L (D E). \end{verbatim}
 
  Note concise representation due to implicit arguments.
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Local Reduction, Negation}
 \[ \ctr{\ianc{\ian{\hypol{\ian{}{A}{u}}{\DD}{p}}{\lnot A}{\noti^{u,p}}
\hspace{4em} \above{\EE}{A}}{C}{\note} }
 \ndredl
  \hypolc{\ian{\EE}{A}{u}}{\relax [C/p]\DD}{C} \]
 %file src/natded/red.elf
 \begin{verbatim}
redl_not : (note (noti D) C E) ==>L (D C E). \end{verbatim}

  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Local Reduction, Universal Quantification}
  \[ \ctr{\ianc{\ian{\above{\DD}{[a/x]A}}{\forall x\ldot
A}{\foralli^a}}{[t/x]A}{\foralle}}
 \ndredl
 \abovec{[t/a]\DD}{[t/x]A} \]
 %file src/natded/red.elf
 \begin{verbatim}
redl_forall :
   (foralle (foralli D) T) ==>L (D T). \end{verbatim}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Higher-Level Judgments}
  \begin{itemize} \itemsep 0pt
   \item Represented as type families indexed by deductions of
lower-level judgments
   \item Requires dependent kinds
   \item Concise with reconstruction
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Meta-Programming and Search}
  Three applications of logical frameworks
  \begin{itemize} \itemsep 0pt
   \item Search within encoded logic
   \item Meta-programming of algorithms
   \item Implement meta-theory
  \end{itemize}

  We mention a few examples below
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Example: Mini-ML}
  [Hannan'89] [Michaylov \& Pf'91] [Pf \& Hannan'92] [Miculan'93]
  \begin{itemize} \itemsep 0pt
   \item Language, type system, operational semantics
   \item Type inference, evaluation
   \item Type preservation: $e \hastype \tau$ and $e \evalsto v$
implies $v \hastype \tau$
  \end{itemize}

  \begin{itemize} \itemsep 0pt
   \item Abstract machine, compilation
   \item Compiler
   \item Compiler correctness
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Example: Logic Programming}
  [Miller et al.'91] [Pf'92] [Dyckhoff'94]
  \begin{itemize} \itemsep 0pt
   \item Language, natural deduction, uniform derivations
   \item Interpreter for queries
   \item Soundness, non-deterministic completeness
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Example: Logical Interpretations}
  [Felty'88] [Pf \& Rohwedder'92] [Pf'94]
  \begin{itemize} \itemsep 0pt
   \item Logic, natural deduction, Hilbert system, sequent system
   \item Search algorithms or tactics
   \item Equivalence of systems, cut-elimination
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Example: Lambda Calculus}
  [Shankar'86] [Pf'92] [Huet'93]
  \begin{itemize} \itemsep 0pt
   \item (Untyped) $\lambda$-calculus, reduction relations
   \item Normalization and conversion
   \item Church-Rosser theorem
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Example: Cartesian Closed Categories}
  [Filinski'92]
  \begin{itemize} \itemsep 0pt
   \item Typed $\lambda$-calculus, CCC's
   \item Equational deduction
   \item Translation
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Example: Set Theory}
  [Paulson'93]
  \begin{itemize} \itemsep 0pt
   \item Language of set theory
   \item Theorem proving tactics
   \item Development of set theory
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Example: Optimizing Program Extraction}
  [Anderson'93]
  \begin{itemize} \itemsep 0pt
   \item Constructive logic, functional language
   \item Program extraction, evaluation, typing
   \item Correctness of extraction
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Search, Choices}
  \begin{itemize}
   \item Goal: hypotheses and conclusion to be proven
   \item Conjunctive choice: all subgoals must be solved, but
in which order?
   \item Disjunctive choice: one alternative must be solved, which one to try?
   \item Universal choice: pick new parameter.
   \item Existential choice: which term do we pick? (e.g. in $\foralle$ or
$\existsi$)
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Tactics and Tacticals}
  LCF [Gordon et al'79], Isabelle [Nipkow \& Paulson'91], $\lambda$Prolog
[Felty'93]
   \begin{itemize} \itemsep 0pt
    \item Widely used (LCF, Nuprl, Coq)
    \item Tactic language embedded in ML or $\lambda$Prolog
    \item Tactics reduce goal to conjunctive subgoals
    \item Inference rules give rise to basic tactics
    \item Tacticals combine tactics to form strategies
    \item Example: disjunctive choice with \verb"tac1 ORELSE tac2"
    \item Useful `weak' method combining interactive and automated
theorem proving
   \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Unification I}
  \begin{itemize} \itemsep 0pt
   \item Unification postpones existential choices during search by
introducing {\bf meta-variables} or {\bf logic variables}
   \item Undecidable in $\lambda^\arrow$ [Huet'73]
   \item Pre-unification practical despite branching [Huet'75]
   \item Built into Isabelle and $\lambda$Prolog
   \item Extends to $\lambda^\Pi$ [Elliott'89,Pym90]
  \end{itemize}
  Example: 
 \[ (\lam x\oftp\lfi \ldot F\, (\lf{s}\, x)) \doteq (\lam x\oftp\lfi
\ldot \lf{s}\, (F\, x)) \]
 Solutions:
 \[ (\lam y\oftp\lfi\ldot \lf{s}\, \ldots (\lf{s}\, y))/F \]
for any number of applications of $\lf{s}$ including zero.
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Unification II}
  Branching and backtracking sometimes undesirable
  \begin{itemize}
   \item Retreat to decidable subcase (higher-order patterns) [Miller'90] [Pf'91] [Nipkow'91]
   \item Maintain `hard' constraints [Pf'91]
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Logic Programming}
   \begin{itemize} \itemsep 0pt
    \item Operational interpretation of hereditary Harrop formulas
($\lambda$Prolog) or types (Elf)
    \item Execution is search for a derivation
    \item Leads to program language, not proof procedure
    \item All choices are made deterministic through depth-first search
combined with unification or constraint solving
    \item Some specifications are directly executable (natural semantics, type
inference)
    \item Not theorem proving, but theorem provers can be programmed
[Felty'88]
    \item Many algorithms are easy to express
    \item Some algorithms are impossible
    \item Mostly a prototyping tool
   \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Automatic Proof Search}
  \begin{itemize}
   \item Unlikely to be feasible in many cases (may need deep properties of
object logic)
   \item General resolution [Huet'76,Paulson'88]
   \item First steps towards other methods via sequent calculi for LF [Pym \&
Wallen'90]
   \item Inductive theorem proving?
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Meta-Theory}
  \begin{itemize} \itemsep 0pt
   \item Derived rules of inference
   \item Admissible rules of inference
   \item Induction over the structure of terms and derivation
   \item Inversion principles
   \item Example: Equivalence of Hilbert calculus and ND
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Derived Rules of Inference}
 \begin{itemize} \itemsep 0pt
  \item Remain valid under all extensions
  \item Representable by defined functions from derivations of premisses to
conclusion
 \end{itemize}
 
 \[ \begin{array}{c}
  \ian{A}{\lnot \lnot A}{{\cf dni}}
 \end{array} \]

  \[ \begin{array}{rcl}
   \lf{dni} & \hastype & \Pi A\oftp\lfo\ldot \lfnd\, A \arrow \lfnd\, (\lf{not}\, (\lf{not}\, A)) \\
   & = & \lam A\oftp\lfo\ldot \lam u\oftp \lfnd\, A \ldot \\
   & & \quad \lf{noti}\, (\lam p\oftp\lfo\ldot \lam w\oftp \lfnd\, (\lf{not}\,
A)\ldot \lf{note}\, w\, p\, u)
  \end{array} \]
 represents
  \sbox{\tempdedA}{\ibn{\ian{}{\lnot A}{v}}{A}{p}{\note}}
 \[ \begin{array}{c}
 \ianc{\usebox{\tempdedA}}{\lnot \lnot A}{\noti^{v,p}}
 \end{array} \]
  \vfill
 \end{slide}



 \begin{slide}{}
  \slidetitle{Hilbert Calculus}
Axiom schemas
 \[ \begin{array}{ll}
   A \limplies (B \limplies A) & (K) \\
   (A \limplies (B \limplies C)) \limplies ((A \limplies B) \limplies (A
\limplies C)) & (S) \\[1ex]
  (A \limplies \lnot B) \limplies ((A \limplies B) \limplies (\lnot A)) &
(N_1) \\
  \lnot A \limplies (A \limplies B) & (N_2) \\[1ex]
  (\forall x\ldot A) \limplies [t/x] A & (F_1) \\
  (\forall x\ldot (B \limplies A)) \limplies (B \limplies \forall x\ldot A) & (F_2)^*
 \end{array} \]
 where $x$ not free in $B$ in rule ($F_2$).  Inference rules
 \[ \begin{array}{c}
  \ibnc{A \limplies B}{A}{B}{(MP)} \hspace{2em}
  \ianc{[a/x] A}{\forall x\ldot A}{UG^a} 
 \end{array} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Hilbert in Elf}
 \begin{verbatim}
hil : fo -> type.

K : hil (A imp (B imp A)).
S : hil ((A imp (B imp C))
          imp ((A imp B) imp (A imp C))).

NOT1 : hil ((A imp (not B))
             imp ((A imp B) imp (not A))).
NOT2 : hil ((not A) imp (A imp B)).

FORALL1 :
   {T:tm} hil ((forall [x:tm] A x) imp (A T)).
FORALL2 : hil ((forall [x:tm] (B imp A x))
               imp (B imp forall [x:tm] A x)).

MP : hil (A imp B) -> hil A -> hil B.
UG : ({a:tm} hil (A a))
      -> hil (forall [x:tm] A x). \end{verbatim}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Occurrence Condition}
 \begin{verbatim}
FORALL2 : hil ((forall [x:tm] (B imp A x))
               imp (B imp forall [x:tm] A x)). \end{verbatim}

 \begin{lfsig}
  \lf{F}_2 & \hastype & \Pi A \oftp \lfi \arrow \lfo\ldot \Pi B\oftp \lfo\ldot \\
 & & \quad \lfhil\, ((\lf{forall}\, (\lam x\oftp\lfi \ldot B \limplies A\, x)) \\
 & & \quad \null \limplies (B \limplies \lf{forall}\, (\lam x\oftp\lfi\ldot
A\, x)))
 \end{lfsig}%

 Substituting a formula $B$ that contains $x$ free would generate capture
($x$ would be renamed).  This encodes the side-condition.
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Hilbert to ND}
  {\bf Theorem} If $\vdhil A$ then $\vdnd A$.

  {\bf Proof:} By induction on the structure of $\abovec{\HH}{\vdhil A}$.
  In each case we construct the corresponding natural deduction
$\abovec{\DD}{\vdnd A}$.  For example:

  {\bf Case:} $\HH = \ianc{}{A\limplies (B \limplies A)}{K}$.  In this
case we have to supply a natural deduction of $A \limplies (B \limplies A)$,
which we have already seen.
 \[ \DD = \ctr{\ianc{\ian{\ian{}{A}{u}}{B \limplies A}{\impi^w}}{A \limplies (B
\limplies A)}{\impi^u}} \]
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Representing Induction}
  Problem: functional representations are not inductive in the ordinary
sense.  Ignoring dependencies:
 \begin{lfsig}
  \lf{impi} & \hastype & (\lfnd \arrow \lfnd) \arrow \lfnd \\
  \lf{impe} & \hastype & \lfnd \arrow \lfnd \arrow \lfnd
 \end{lfsig}%
 Note negative occurrence of $\lfnd$ in $\lf{impi}$.

 Similarly, for dependent functions.
 \begin{lfsig}
 \lf{foralli} & \hastype & \Pi A\oftp \lfi \arrow \lfo\ldot \\
 & & \quad (\Pi a\oftp \lfi \ldot \lfnd\; (A\; a)) \arrow \lfnd\;
(\lf{forall}\; A)
 \end{lfsig}%
 If $\Pi a\oftp \lfi \ldot \lfnd\; (A\; a)$ can be proved by induction, this
is an encoding of an $\omega$-rule.  There may not be a parametric derivation
of the judgment $\vdnd [a/x]A$, but only different derivations of $[t/x]A$ for
each $t$.
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Prim.~Recursion and HOAS}
 Assume $\lfi$ is fixed to be the natural numbers and $p\oftp \lfo$.
Define $f \hastype \lfi \arrow \lfo$ by primitive recursion.
 \[ \begin{array}{rcl}
  f\, (\lf{z}) & = & \lf{imp}\, p\, p \\
  f\, (\lf{s}\, x) & = & \lf{forall}\, (\lam x\oftp \lfi\ldot p)
 \end{array} \]
 Then
 \[ \lf{foralli}\, (\lam x\oftp A\ldot f\, x) \hastype \lfo, \]
 but this object has no canonical form and does not represent
an object language formula.
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Inductive Meta-Theory}
 \begin{itemize}
  \item Frameworks based on inductive definitions\\
   FS0 [Feferman'87] [Matthews et al'93] \\
   ALF [Magnusson \& Nordstr\"om'94] \\
   No higher-order abstract syntax
  \item Partial inductive definitions [Halln\"as'87]\\
   Pi [Eriksson'94] [Schroeder-Heister'93] \\
   Automatic construction of eliminations
  \item Use of general systems with induction as frameworks \\
   NQTHM [Shankar'86] \\
   Nuprl [Basin \& Constable'93] \\
   Coq [Huet'93] \\
   LEGO [Pollack'93]
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Externalizing Induction}
 \begin{itemize} \itemsep 0pt
  \item G\"odel's T externalizes induction
  \item A function is total, since it is presented as a primitive recursion
  \item Here: implement the relation between Hilbert deduction and natural
deductions as a higher-level judgment
  \item Captures computational content of meta-proof
  \item Executable as logic program
  \item Check that this judgment is ``primitive recursive''
for verification \\ \relax
        [Pf \& Rohwedder'92] [Rohwedder'94]
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Hilbert to ND, K}
 \begin{lfsig}
  \lf{hilnd} & \hastype & \Pi A\oftp \lfo\ldot \lfhil\, A \arrow
\lfnd\, A \arrow \type
 \end{lfsig}%
 \begin{verbatim}
hilnd : hil A -> nd A -> type. \end{verbatim}

  {\bf Case:} $\HH = \ianc{}{A\limplies (B \limplies A)}{K}$.  In this
case we have to supply a natural deduction of $A \limplies (B \limplies A)$,
which we have already seen.
 \[ \DD = \ctr{\ianc{\ian{\ian{}{A}{u}}{B \limplies A}{\impi^w}}{A \limplies (B
\limplies A)}{\impi^u}} \]
 \begin{verbatim}
hnd_K :
  hilnd (K) (impi [u:nd A] impi [v:nd B] u). \end{verbatim}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Hilbert to ND, S}
  {\bf Case:} $\HH = \ianc{}{(A \limplies (B \limplies C)) \limplies ((A
\limplies B) \limplies (A \limplies C))}{S}$.  A natural deduction of
the conclusion is

 \sbox{\tempdedA}{\ian{\ian{\ian{}{A \limplies (B \limplies
C)}{u}\hspace{2em}\ian{}{A}{w}}{B \limplies C}{\impe} \hspace{10em}
\ibn{\ian{}{A \limplies B}{v}}{\ian{}{A}{w}}{B}{\impe}}{C}{\impe}}
 \[ \ian{\ian{\ian{\usebox{\tempdedA}
}{A \limplies C}{\impi^w}
}{(A \limplies B) \limplies (A \limplies C) }{\impi^v} }{(A
\limplies (B \limplies C)) \limplies ((A \limplies B) \limplies (A \limplies
C))}{\impi^u} \]

 In Elf:
 \begin{verbatim}
hnd_S : hilnd (S)
         (impi [u:nd (A imp B imp C)]
          impi [v:nd (A imp B)]
          impi [w:nd A] impe (impe u w)
                             (impe v w)). \end{verbatim}
 \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Hilbert to ND, Axioms}
 \begin{small}
\begin{verbatim}
hnd_NOT1 : hilnd (NOT1)
                 (impi [u:nd (A imp (not B))]
                  impi [v:nd (A imp B)]
                  noti [p:fo] [w:nd A]
                  note (impe u w) p (impe v w)).

hnd_NOT2 : hilnd (NOT2) (impi [u:nd (not A)]
                           impi [v:nd A] note u B v).

hnd_FORALL1 :
  hilnd (FORALL1 T)
        (impi [u:nd (forall [x:tm] A x)] foralle u T).

hnd_FORALL2 :
  hilnd (FORALL2)
    (impi [u:nd (forall [x:tm] (B imp A x))]
     impi [v:nd B]
     foralli [a:tm] impe (foralle u a) v). \end{verbatim}
 \end{small}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Hilbert to ND, MP}
  {\bf Case:} $\HH = \ibnc{\above{\HH_1}{A\limplies
B}}{\above{\HH_2}{A}}{B}{MP}$.  By induction hypothesis on $\HH_1$ and $\HH_2$
there exists natural deduction $\DD_1 \of A \limplies B$ and $\DD_2 \of A$,
respectively.  Using the rule of implication elimination $\impe$, we obtain
 \[ \DD = \ibnc{\above{\DD_1}{A\limplies B}}{\above{\DD_2}{A}}{B}{\impe} \]
 \begin{verbatim}
hnd_MP : hilnd (MP H1 H2) (impe D1 D2)
          <- hilnd H1 D1
          <- hilnd H2 D2. \end{verbatim}
 (Recall $A_3 \leftarrow A_2 \leftarrow A_1$ equals $A_1 \arrow A_2 \arrow
A_3$)
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Hilbert to ND, UG}
 {\bf Case:} $\HH = \ianc{\above{\HH_1}{[a/x]A}}{\forall x\ldot A}{UG^a}$.
By induction hypothesis on $\HH_1$ there exists a natural
deduction $\DD_1 \of [a/x]A$.  We construct
 \[ \DD = \ianc{\above{\DD_1}{[a/x]A}}{\forall x\ldot A}{\foralli^a} \]

 \begin{verbatim}
hnd_UG : hilnd (UG H1) (foralli D1)
            <- {a:tm} hilnd (H1 a) (D1 a). \end{verbatim}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Computational Meta-Theory}
 \begin{verbatim}
?- hilnd (MP (MP S K) K) D.

D =
   impe
      (impe
          (impi [u:nd (A imp (B imp A) imp A)]
              impi [v:nd (A imp B imp A)]
              impi [w:nd A]
              impe (impe u w) (impe v w))
          (impi [u:nd A]
              impi [v:nd (B imp A)] u))
      (impi [u:nd A] impi [v:nd B] u).
;
no more solutions \end{verbatim}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Meta-Proofs as Judgments}
  \begin{itemize} \itemsep 0pt
   \item Externalize induction (schema-checking, work in progress)
   \item Computationally adequate
   \item Applied in many examples
  \end{itemize}
  Alternatives (work in progress)
  \begin{itemize} \itemsep 0pt
   \item HOAS plus induction [Despeyroux \& Hirschowitz'94]
   \item Theory of binding [Talcott] [Matthews]
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{The Deduction Theorem}
  Write $A_1,\ldots,A_n \vdhil B$ for hypothetical Hilbert judgment.
Use $\Delta$ for $A_1,\ldots,A_n$.

 {\bf Theorem} (Deduction Theorem)
  If $\Delta, A \vdhil B$ then $\Delta \vdhil A \limplies B$.

 {\bf Proof:} By induction on the structure of $\above{\HH}{\Delta,A \vdhil
B}$.  In the implementation we can ignore $\Delta$, since it remains
fixed throughout the proof.  The representing type family:

  \begin{lfsig}
  \lf{ded} & \hastype & \Pi A\oftp\lfo\ldot \Pi B\oftp\lfo\ldot\\
 & & \quad (\lfhil\, A \arrow \lfhil\, B) \arrow \lfhil (\lf{imp}\, A\, B)\\
 & & \quad \null \arrow \type.
 \end{lfsig}%

 \begin{verbatim}
ded : (hil A -> hil B) -> hil (A imp B)
       -> type. \end{verbatim}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Ded~Thm, Hypothesis}
   {\bf Case:} $\HH = \Delta, A \vdhil A$, that is, $\HH$ consists of a use of
the hypothesis $A$.  Then we need to show that $\Delta \vdhil A \limplies A$.
This follows by two applications of Modus Ponens from $(S)$ and $(K)$.
Written in linear form instead of the more awkward tree we have
  \[ \begin{array}{llr}
  1 & (A \limplies ((B \limplies A) \limplies A)) \\
    & \null \limplies ((A \limplies (B \limplies A)) \limplies (A \limplies
A)) & S \\
  2 & (A \limplies ((B \limplies A) \limplies A)) & K \\
  3 & (A \limplies (B \limplies A)) \limplies (A \limplies A) & MP\, 1\, 2 \\
  4 & A \limplies (B \limplies A) & K \\
  5 & A \limplies A & MP\, 3\, 4
  \end{array} \]
 %file elf/metatheory.elf
 \begin{verbatim}
ded_ID : ded ([u:hil A] u) (MP (MP S K) K). \end{verbatim}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Ded~Thm, Axiom}
 {\bf Case:} $\HH = \ianc{}{\Delta, A \vdhil B_1 \limplies (B_2 \limplies
B_1)}{K}$.  Then
 \[ \begin{array}{rlr}
  1 & \Delta \vdhil (B_1 \limplies (B_2 \limplies B_1))\\
 & \quad \null \limplies (A \limplies (B_1 \limplies (B_2 \limplies B_1))) & K
\\
  2 & \Delta \vdhil B_1 \limplies (B_2 \limplies B_1) & K \\
  3 & \Delta \vdhil A \limplies (B_1 \limplies (B_2 \limplies B_1)) & MP\, 1\,
2
 \end{array} \]
 %file elf/metatheory.elf
 \begin{verbatim}
ded_K : ded ([u:hil A] K) (MP K K). \end{verbatim}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Ded~Thm, MP}
  {\bf Case:} \[ \HH = \ibnc{\above{\HH_1}{\Delta, A \vdhil B_1 \limplies
B_2}}{\above{\HH_2}{\Delta, A \vdhil B_1}}{\Delta, A \vdhil B_2}{MP.} \]
 \[ \begin{array}{rlr}
  1 & \Delta \vdhil A \limplies (B_1 \limplies B_2) & \mbox{IH~on
$\HH_1$} \\
  2 & \Delta \vdhil (A \limplies (B_1 \limplies B_2)) \\
  & \quad \null \limplies ((A \limplies
B_1) \limplies (A \limplies B_2)) & S \\
  3 & \Delta \vdhil (A \limplies B_1) \limplies (A \limplies B_2) & MP\; 2\; 1
\\
  4 & \Delta \vdhil A \limplies B_1 & \mbox{IH~on $\HH_2$} \\
  5 & \Delta \vdhil A \limplies B_2 & MP\; 3\; 4
 \end{array} \]
 %file elf/metatheory.elf
 \begin{verbatim}
ded_MP : ded ([u:hil A] MP (H1 u) (H2 u))
             (MP (MP S H1') H2')
          <- ded H1 H1'
          <- ded H2 H2'. \end{verbatim}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Ded~Thm, Complete}
 \begin{small}
 \begin{verbatim}
ded : (hil A -> hil B) -> hil (A imp B) -> type.

ded_ID : ded ([u:hil A] u) (MP (MP S K) K).

ded_K : ded ([u:hil A] K) (MP K K).
ded_S : ded ([u:hil A] S) (MP K S).

ded_NOT1 : ded ([u:hil A] NOT1) (MP K NOT1).
ded_NOT2 : ded ([u:hil A] NOT2) (MP K NOT2).

ded_FORALL1 : ded ([u:hil A] FORALL1 T)
                  (MP K (FORALL1 T)).
ded_FORALL2 : ded ([u:hil A] FORALL2)
                  (MP K FORALL2).

ded_MP : ded ([u:hil A] MP (H1 u) (H2 u))
             (MP (MP S H1') H2')
          <- ded H1 H1'
          <- ded H2 H2'.

ded_UG : ded ([u:hil A] UG (H1 u))
             (MP FORALL2 (UG H1'))
            <- {a:tm} ded ([u:hil A] H1 u a) (H1' a). \end{verbatim}
 \end{small}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Summary: Syntax}
   \begin{itemize} \itemsep 0pt
    \item Uni-typed vs simply-typed representation
    \item External vs internal validity
    \item Variables as constants, de Bruijn indices, or meta-variables
    \item Higher-order abstract syntax:
    \begin{itemize}
     \item Expressions $\Longrightarrow$ canonical forms
     \item Renaming $\Longrightarrow$ $\alpha$-conversion
     \item Substitution $\Longrightarrow$ $\beta$-reduction
    \end{itemize}
    \item Inductive vs open-ended representation
   \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Summary: Deductions}
  \begin{itemize} \itemsep 0pt
   \item Derivability vs deductions-as-objects
   \item External vs internal validity
   \item ($\lambda^\arrow$+hhf) vs ($\lambda^\pi$)
   \item $\lambda$Prolog, Isabelle vs Elf
   \item LF: Judgments-as-types
   \item Hypothetical judgments as functions
   \item Parametric judgments as functions
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Summary: Meta-Programming}
  \begin{itemize} \itemsep 0pt
   \item Tactics and tacticals in ML
   \item Direct interpretation as constraint logic programming
   \item Higher-order unification vs constraint simplification
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Summary: Meta-Theory}
 \begin{itemize} \itemsep 0pt
  \item HOAS vs inductive definitions
  \item External vs internal validity
  \item Computational meta-theory
  \item Partial inductive definitions
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Implementations}
 \begin{itemize} \itemsep 0pt
  \item Isabelle [Nipkow \& Paulson]
  \item $\lambda$Prolog [Nadathur \& Miller]
  \item Elf [Pf.]
  \item ALF [Magnusson \& Nordstr\"om]
  \item FS0 [Matthews]
  \item Pi [Eriksson]
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Some Current Issues}
 \begin{itemize} \itemsep 0pt
  \item HOAS and induction
  \item Subtyping
  \item Substructural frameworks
  \item Equality
  \item Modularity
  \item User interfaces
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Conclusion}
 \begin{itemize} \itemsep 0pt
  \item Deductive systems as a common conceptual tool
  \item Logical frameworks to aid understanding and support implementation
 \end{itemize}
  \vfill
 \end{slide}
\end{document}