LF2TeX project

LF2TeX is a tool for visualizing logic constraints (Twelf code) as natural deductions (proof trees in TeX). This tool takes a formal language specification in Twelf and a customizable typesetting specification in TeX to produces rules and deduction for the syntax, semantics and proofs of the language. The tool can also generate proofs in a numbered point format, which is more compact.
  1. Demo for simply-typed lambda calculus
  2. Demo for noninterference theorem for DCC: pdf, elf, ref
  3. Demo for dynamic updating of information-flow policies: pdf, elf, ref
  4. Demo for Apollo the security-typed language: pdf, elf, ref
  5. Demo for de Bruijn index representation: pdf, elf
  6. Demo for featherweight Java: pdf, elf, ref
  7. Demo for confluence theorem: pdf, elf, ref

  8. Package download: lf2tex-0.2.tgz
  9. Requirements and resources 


LF2TeX is a tool for visualizing logic constraints (Twelf code) as
natural deductions (proof trees in TeX). This tool takes a formal
language specification in Twelf and a customizable typesetting
specification in TeX to produces rules and deduction for the syntax,
semantics and proofs of the language. The tool can also generate
proofs in a numbered point format, which is more compact.


----------------------------------------
Quick Start
----------------------------------------

> tar zxvf ocaml-3.08.tgz    # and install...
> tar zxvf twelf-1.5.tgz     # and install...

> cp twelf/bin/twelf-server /usr/bin
> tar zxvf lf2tex-0.2.tgz
> cd lf2tex-0.2
> make lambda.dvi
> xdvi lambda.dvi


----------------------------------------
Outline
----------------------------------------

- TeX output (lambda.dvi)
- language specification (lambda.elf)
- proof construction (main.ml)
- typesetting specification (lambda.tin)
- processing phases (lf2tex.sh)
- LF challenges
- TeX challenges
- resources


lambda.elf lambda.tin
  Soundness theorem for simply-typed lambda calculus
  in abstract variable representation

conflu.elf conflu.tin
  Confluence theorem for simply-typed lambda calculus
  with Barendregt Variable Convention

index.elf index.tin
  Soundness theorem for simply-typed lambda calculus
  in de Bruijn index representation

apollo.elf apollo.tin
  Soundness theorem for security-typed language
  http://www.cis.upenn.edu/~stse/apollo

lf2tex.s sugar.el
  Concrete syntax definition and its Emacs mode used by the tool "sugar" [3]
  to generate compiler files: parse.mly print.ml scan.mll sugar.ml
  http://www.cis.upenn.edu/~stse/sugar

parse.mly print.ml scan.mll sugar.ml main.ml lf2tex.sh
  Compiler for LF to TeX


----------------------------------------
Language Specification (lambda.elf)
----------------------------------------

A language is specified in Twelf [4,5], the meta-logical
framework. LF2TeX [1] then determines the _kind_ of a LF term from its
LF type and generates the corresponding TeX code. LF2TeX does not
handle higher-order abstract syntax; we prefer abstract variable or de
Bruijn index representations that allow direct formalizations of our
languages.


1. Syntax classes
   
    [Kind] type
  
    [LF]   t : type.  
    [TeX]  t ::= ...       (t)
  
2. Syntax definitions 

    [Kind] a1 -> a2 -> ..    where a1 is a syntax

    [LF]   tfun : t -> t -> t.
    [TeX]  t ::= t -> t    (tfun)

3. Definitional equalities
 
    [Kind] type  

    [LF]   p = t : type.
    [TeX]  p = t.          (p)

4. Judgement schemes

    [Kind] a1 -> a2 -> .. -> type    where a1 is a syntax
  
    [LF]   ty : g -> e -> t -> type.
    [TeX]  g |- e : t      (ty)

5. Judgement axioms

    [Kind] a1 a2.. where a1 is a judgement
  
    [LF]   ty-unit : ty G unit tunit.
    [TeX]  g |- <> : <>    (ty-unit)

6. Judgement rules

    [Kind] a1 a2.. <- a3 a4..    where a1 is a judgement
  
    [LF]   ty-fun : ty G (fun T1 E) (tfun T1 T2)
             <- ty (gt G T1) E T2.

    [TeX]  g,x:t1 |- fun x:t1.e : t2
           ---------------------------  (ty-fun)
           g |- fun x:t1.e : t1 -> t2

7. Theorem statements 

    [Kind] a1 a2 -> a3 a4 -> .. -> type    where a1 is a judgement
  
    [LF]   pg : ty gn E T -> evval E -> type.

    [TeX]  . |- e : t
           ---------------------------  (ps)
           evval e

8. Theorem proofs

    [Kind] a1 a2 -> a3 a4 -> ..    where a1 is a theorem
  
    [LF]   ps-app1 : ps (ty-app Ty2 Ty1) (ev-app1 Ev) (ty-app Ty2 Ty3)
             <- ps Ty1 Ev Ty3.

    [LF*]  {G:g} {E1:e} {T1:t} {T2:t} {E2:e} {E3:e}
           {Ty1:ty G E1 (tfun T1 T2)}
           {Ty2:ty G E3 T1}
           {Ev:ev E1 E2}
           {Ty3:ty G E2 (tfun T1 T2)}

           ps G E1 (tfun T1 T2) E2 Ty1 Ev Ty3
           -> ps G (app E1 E3) T2 (app E2 E3) (ty-app G E3 T1 E1 T2 Ty2 Ty1)
              (ev-app1 E1 E2 E3 Ev) (ty-app G E3 T1 E2 T2 Ty2 Ty3).

    [TeX]  

  g |- e1 e3 : t2           e1 e3 --> e2 e3
  ---------------- *ty-app  --------------- *ev-app
  g |- e1 : t1->t2          e1 -> e2       g |- e1 e3 : t2
  ------------------------------------ ps  --------------- *ty-app
  g |- e2 : t1->t2                         g |- e3 : t1
  ------------------------------------------------------------ ty-app     (ps)
  g |- e2 e3 : t


----------------------------------------
Proof Construction (main.ml)
----------------------------------------

The core of LF2TeX is to reconstruct a theorem proof as a natural
deduction from its representation as a dependently-typed LF term. The
two key challenges are handling implicit inversions and introducing
auxiliary variables to explicitly annotate the types of all subterms.

Every LF proof term can be separated into its conclusion parts and its
premise parts. In order to represent proofs as trees, LF2TeX only
handles proof terms having multiple input but only one
output. Therefore, LF2TeX can regard the last parameter to be the
output and the rest to be the input.

LF2TeX uses the type of a subterm to represent a step in its proof
tree. To obtain the type of all subterms without implementing the LF
type-checking algorithm, LF2TeX first makes the input and output of
all inference rules atomic by introducing auxiliary variables and
keeping tracks of their types. The table of these atomic rules also
facilitate the linear search procedure of constructing a proof tree.


ps-app1 : ps (ty-app Ty2 Ty1) (ev-app1 Ev) (ty-app Ty2 Ty3)
  <- ps Ty1 Ev Ty3.

- Conclusion:          ps (ty-app Ty2 Ty1) (ev-app1 Ev) (ty-app Ty2 Ty3)
- Conclusion input:    (ty-app Ty2 Ty1) (ev-app1 Ev)
- Conclusion output:   (ty-app Ty2 Ty3)

- Premise:             ps Ty1 Ev Ty3
- Premise input:       Ty1 Ev
- Premise output:      Ty3


** reduce a LF proof to a table of atomic input and output

Goal: _1

_1   =  ty-app Ty2 Ty3
Ty1  =  *ty-app _2
Ty2  =  *ty-app _2
_2   =  ...
Ev   =  *ev-app1 _3
_3   =  ...
Ty3  =  ps Ty1 Ev


1. Conclusion input:   f X1 X2 Y -> f [] Y, "" X1, "" X2
2. Conclusion output:  f X (g Y1 Y2) -> f X Z, g Y1 Y2 Z
3. Premise input:      f (g X1 X2) Y ---> f Z Y, g X1 X2 Z
4. Premise output:     f X (g Y1 Y2) --> f X Z, *g Z Y1, *g Z Y2


Some notes about the layout of proof trees:
- unused premises are listed on the top with vertical dots, showing
  the canonical forms of the input
- implicit applications of inversions and canonical forms are prefixed
  with downarrows in the rule names
- wide lists of premises are broken into vertical arrays with aligned
  bullets on the left.


----------------------------------------
Typesetting Specification (lambda.tin)
----------------------------------------

To be able to generate _all_ the typesetting of the language, LF2TeX
requires the specification of _only_ the following LF terms: syntax
classes (e, t, g, ...), syntax definitions (arrow, variable, fun,
...), and judgement schemes (g |- e : t and e -> e).

The typesetting can be specified directly in plain TeX or LaTeX (with
the "z" prefix for namespace). But we choose to have another lexical
translator, called Tinker [2], that automatically handles expression
subscripting and spacing.


1. Syntax classes:

  [LF]      e : type.
  [Tinker]  \newcommand{\ze}[0]{@e@}
  [TeX]     \newcommand{\ze}[0]{\ensuremath{\N{e}}}

2. Syntax definitions: 

  [LF]      fun : t -> e -> e.
  [Tinker]  \newcommand{\zfun}[2]{@fun x:#1.#2@}
  [TeX]     \newcommand{\zfun}[2]{\ensuremath{\lambda \N{x}\!:\!#1.#2}}

3. Judgement schemes:

  [LF]      ty : g -> e -> t -> type.
  [Tinker]  \newcommand{\zty}[3]{@#1 |- #2 : #3@}
  [TeX]     \newcommand{\zty}[3]{\ensuremath{#1 \vdash #2 : #3}}
  

----------------------------------------
Processing Phases (lf2tex.sh)
----------------------------------------

1.  twelf  : foo.elf  --> foo.elf2      print implicit arguments
2.  lf2tex : foo.elf2 --> foo.tex0      syntax, rules, theorems, proofs
3.  tinker : foo.tex0 --> foo.tex1      expression subscripting and spacing
4.  escape : foo.elf  --> foo.sed       section headers
5.  sed    : foo.tex1 --> foo.tex2      applying foo.sed
6.  latex  : foo.tin  --> foo.dvi       all together


----------------------------------------
LF Challenges
----------------------------------------

- better variable numbering in term/type reconstruction
- state and prove lemmas for canonical forms, inversion
- coinduction, logical relations, noninterference
- arbitrary meta assertion: termination and mode
- default mode, auto termination specification
- termination metric, more powerful totality check
- object-level negation, object-level totality
- handle higher-order abstract syntax
- handle higher-order judgements


----------------------------------------
TeX Challenges
----------------------------------------

- better way to represent unused premises
- better way to represent canonical forms
- calculate typesetting bound for wide inference rules
- parenthesize non-atomic terms


----------------------------------------
Resources
----------------------------------------

[1] LF2TeX: visualize LF code as trees in TeX 
    http://www.cis.upenn.edu/~stse/lf2tex

[2] Tinker: typesetting lambda calculi in TeX
    http://www.cis.upenn.edu/~stse/index.html#tinker

[3] Sugar: concrete syntax grammar
    http://www.cis.upenn.edu/~stse/sugar

[4] Twelf: meta-logical framework
    http://www.twelf.org

[5] Computation and Deduction, Frank Pfenning
    http://www.cs.cmu.edu/~fp/courses/comp-ded/handouts/cd.ps


Stephen Tse 
July 30th, 2004, version 0.1
April 7th, 2005, version 0.2

Last modified: Sat Jul 31 09:43:19 EDT 2004