Justification for lambda calculus embedding.
-rw-r--r-- 78 .gitignore
drwxr-xr-x - Diagrams
-rw-r--r-- 1068 Makefile
-rw-r--r-- 2401 abstract.tex
-rw-r--r-- 1682 conclusion.tex
-rw-r--r-- 1633 fhm-preamble-extras.fmt
-rw-r--r-- 683 fhm-preamble.fmt
-rw-r--r-- 1603 future.lhs
-rw-r--r-- 15108 introduction.tex
-rw-r--r-- 42406 llncs.cls
-rw-r--r-- 1480 llncsdoc.sty
-rw-r--r-- 15251 mathpartir.sty
-rw-r--r-- 10345 modular-equations.lhs
-rw-r--r-- 6061 related-work.lhs
-rw-r--r-- 4781 tfp-paper.bib
-rw-r--r-- 2113 tfp-paper.lhs
-rw-r--r-- 24314 type-system.lhs