Commit 3af27bc2 authored by Navid Roux's avatar Navid Roux 💬 Committed by Michael Kohlhase
Browse files

Archive my logrel talk: add sources for reproducibility, link to YouTube video

parent 81e95beb
# N. Roux: “A Beginner's Guide to Logical Relations for a Logical Framework”
Based on [“Logical Relations for a Logical Framework”]( (ACM Transactions on Computational Logic (2013)) by Rabe and Sojakova, Navid Roux delivered a talk and wrote a guide on motivating, introducing, and representing logical relations in the [MMT system](
- **Manuscript/Guide:** [./guide.pdf](./guide.pdf) (submitted 2021-03-22)
- **Talk:** <> (post-recorded)
Meta data of the official, unrecorded talk:
- Title: Logical Relations for a Logical Framework
- Presenter: Navid Roux
- Date: 2021-01-27 14:45 - 16:15 CET
- Place: virtual in Zoom meeting
- **Slides:** [./slides.pdf](./slides.pdf) (submitted 2021-01-27)
LaTeX Sources are contained in [`./sources`](./sources). See [`./sources/`](./sources/ for building.<br>
(Note to core kwarc members: the sources are manually mirrored, hopefully consistently, at <>.)
## Abstract
> Logical relations are an established proof technique for deriving meta-level theorems of formal systems. For example, they have been used to prove strong normalization, type safety, and correctness
> of compiler optimizations in the setting of various type theories and lambda calculi. Theories of
> logical relations have been stated for a wide range of formal systems.
> To formalize formal systems themselves, logical frameworks have been sucessfully used, particularly shining when specifying syntax and deduction (e.g. using judgements-as-types and higherorder abstract syntax). And module systems over logical frameworks allow to modularly identify,
> translate, and combine full hierarchies of formal systems.
> How to represent logical relations in such systems is an ongoing research question. In [“Logical
> Relations for a Logical Framework”]( (ACM Transactions on Computational Logic (2013)), Rabe
> and Sojakova present a theory of logical relations applicable in the setting of logical frameworks
> that, when instantiated for formal systems formalized therein, gives a reasonable notion of logical
> relations within those systems.
> **We provide a detailed exposition of a special case, accessible to everyone familiar with basics
> of formalizing in logical frameworks.** Our exposition is embedded in a coherent narrative spanning
> from concretely motivating logical relations (by walking through a proof of strong normalization
> for the simply-typed lambda calculus) up to concretely modeling a corresponding language feature
> for the [MMT module system]( over the Edinburgh Logical Framework. **The mechanics of our derived
> language feature are novel and forgo the need of introducing any logical relation-specific language
> primitive.**
# from the comments package
use Config;
if (not exists $ENV{'TEXINPUTS'}) {
$ENV{'TEXINPUTS'} = $ENV{'TEXINPUTS'} . $Config{path_sep} . '..' . $Config{path_sep};
# Use LuaLaTeX:
$pdf_mode = 4;
$postscript_mode = $dvi_mode = 0;
# TexStudio doesn't reecognize changed PDF output name in internal PDF viewer
# $jobname = 'Master-Project-Diagram-Operators';
# $lualatex = 'xelatex.exe -no-pdf -shell-escape -synctex=1 -8bit %O %S';
$out_dir = 'build';
\ No newline at end of file
# Slides and Manuscript for “A Beginner's Guide to Logical Relations for a Logical Framework”
The main files are `slides.tex` and `report.tex`. Follow the `% !TEX TS-program` meta directive in the respective file for building.
Prebuilt PDFs can be found in `./build`:
- [latest version](./build/slides.pdf), and [same with Beamer notes](./build/slides-with-notes.pdf)
- [version presented in official talk 2021-01-27](./build/slides-2021-01-27-presented-version.pdf), and [same with Beamer notes](./build/slides-2021-01-27-presented-version-with-notes.pdf)
For the slides, there are two versions you can build: one without and one with attached Beamer notes. Comment or uncomment the respective line `\setbeameroption{show notes on second screen}` in `slides.tex` to switch between both variants.
## How to update anything (make corrections)
1. For the slides:
1. Activate notes as described above.
2. Build as hinted at above, then move `./build/slides.pdf` to `./build/slides-with-notes.pdf`.
3. Deactivates notes.
4. Build. (And leave generated `./build/slides.pdf` as-is.)
2. For the report (aka manuscript, guide): build as hinted at above.
3. For everything: copy the updated files `./build/slides.pdf` and `./build/report.pdf` to <> (as `slides.pdf` and `guide.pdf`, respectively) and keep the sources there synced with the sources here.
\ No newline at end of file
; DO NOT EDIT (unless you know what you are doing)
; This subdirectory is a git "subrepo", and this file is maintained by the
; git-subrepo command. See
remote =
branch = master
commit = 7098dbecfefc25585680dfe04b6f4fb364649c84
parent = bea08dab19c3b2800b73b0fe2f34c3c789ddb6aa
method = merge
cmdver = 0.4.3
language: generic # don't install any environment
os: linux
dist: xenial
script: /bin/bash src/travis/
- ENCRYPTION_LABEL: "80dbef1467b0"
CC0 1.0 Universal
Statement of Purpose
The laws of most jurisdictions throughout the world automatically confer
exclusive Copyright and Related Rights (defined below) upon the creator and
subsequent owner(s) (each and all, an "owner") of an original work of
authorship and/or a database (each, a "Work").
Certain owners wish to permanently relinquish those rights to a Work for the
purpose of contributing to a commons of creative, cultural and scientific
works ("Commons") that the public can reliably and without fear of later
claims of infringement build upon, modify, incorporate in other works, reuse
and redistribute as freely as possible in any form whatsoever and for any
purposes, including without limitation commercial purposes. These owners may
contribute to the Commons to promote the ideal of a free culture and the
further production of creative, cultural and scientific works, or to gain
reputation or greater distribution for their Work in part through the use and
efforts of others.
For these and/or other purposes and motivations, and without any expectation
of additional consideration or compensation, the person associating CC0 with a
Work (the "Affirmer"), to the extent that he or she is an owner of Copyright
and Related Rights in the Work, voluntarily elects to apply CC0 to the Work
and publicly distribute the Work under its terms, with knowledge of his or her
Copyright and Related Rights in the Work and the meaning and intended legal
effect of CC0 on those rights.
1. Copyright and Related Rights. A Work made available under CC0 may be
protected by copyright and related or neighboring rights ("Copyright and
Related Rights"). Copyright and Related Rights include, but are not limited
to, the following:
i. the right to reproduce, adapt, distribute, perform, display, communicate,
and translate a Work;
ii. moral rights retained by the original author(s) and/or performer(s);
iii. publicity and privacy rights pertaining to a person's image or likeness
depicted in a Work;
iv. rights protecting against unfair competition in regards to a Work,
subject to the limitations in paragraph 4(a), below;
v. rights protecting the extraction, dissemination, use and reuse of data in
a Work;
vi. database rights (such as those arising under Directive 96/9/EC of the
European Parliament and of the Council of 11 March 1996 on the legal
protection of databases, and under any national implementation thereof,
including any amended or successor version of such directive); and
vii. other similar, equivalent or corresponding rights throughout the world
based on applicable law or treaty, and any national implementations thereof.
2. Waiver. To the greatest extent permitted by, but not in contravention of,
applicable law, Affirmer hereby overtly, fully, permanently, irrevocably and
unconditionally waives, abandons, and surrenders all of Affirmer's Copyright
and Related Rights and associated claims and causes of action, whether now
known or unknown (including existing as well as future claims and causes of
action), in the Work (i) in all territories worldwide, (ii) for the maximum
duration provided by applicable law or treaty (including future time
extensions), (iii) in any current or future medium and for any number of
copies, and (iv) for any purpose whatsoever, including without limitation
commercial, advertising or promotional purposes (the "Waiver"). Affirmer makes
the Waiver for the benefit of each member of the public at large and to the
detriment of Affirmer's heirs and successors, fully intending that such Waiver
shall not be subject to revocation, rescission, cancellation, termination, or
any other legal or equitable action to disrupt the quiet enjoyment of the Work
by the public as contemplated by Affirmer's express Statement of Purpose.
3. Public License Fallback. Should any part of the Waiver for any reason be
judged legally invalid or ineffective under applicable law, then the Waiver
shall be preserved to the maximum extent permitted taking into account
Affirmer's express Statement of Purpose. In addition, to the extent the Waiver
is so judged Affirmer hereby grants to each affected person a royalty-free,
non transferable, non sublicensable, non exclusive, irrevocable and
unconditional license to exercise Affirmer's Copyright and Related Rights in
the Work (i) in all territories worldwide, (ii) for the maximum duration
provided by applicable law or treaty (including future time extensions), (iii)
in any current or future medium and for any number of copies, and (iv) for any
purpose whatsoever, including without limitation commercial, advertising or
promotional purposes (the "License"). The License shall be deemed effective as
of the date CC0 was applied by Affirmer to the Work. Should any part of the
License for any reason be judged legally invalid or ineffective under
applicable law, such partial invalidity or ineffectiveness shall not
invalidate the remainder of the License, and in such case Affirmer hereby
affirms that he or she will not (i) exercise any of his or her remaining
Copyright and Related Rights in the Work or (ii) assert any associated claims
and causes of action with respect to the Work, in either case contrary to
Affirmer's express Statement of Purpose.
4. Limitations and Disclaimers.
a. No trademark or patent rights held by Affirmer are waived, abandoned,
surrendered, licensed or otherwise affected by this document.
b. Affirmer offers the Work as-is and makes no representations or warranties
of any kind concerning the Work, express, implied, statutory or otherwise,
including without limitation warranties of title, merchantability, fitness
for a particular purpose, non infringement, or the absence of latent or
other defects, accuracy, or the present or absence of errors, whether or not
discoverable, all to the greatest extent permissible under applicable law.
c. Affirmer disclaims responsibility for clearing rights of other persons
that may apply to the Work or any use thereof, including without limitation
any person's Copyright and Related Rights in the Work. Further, Affirmer
disclaims responsibility for obtaining any necessary consents, permissions
or other rights required for any use of the Work.
d. Affirmer understands and acknowledges that Creative Commons is not a
party to this document and has no duty or obligation with respect to this
CC0 or use of the Work.
For more information, please see
### <CONFIG> ###
# BIB files = kwarccrossrefs.bib extcrossrefs.bib
bib.kcr = kwarcpubs.bib $(
bib.ext = extpubs.bib $(bib.kcr)
bib.all = preamble.bib $(bib.ext)
bib.people = mkohlhase akohlhase miancu dginev cjucovschi twiesing dmueller frabe cprodescu clange cdavid vzholudev cmueller nmueller fhorozal jbetzendahl tpollinger mrapp kbercic cshi mrupprecht jfschaefer nroux rmarcus = sissi tetrapod TNTBase arXMLiv cpoint jomdoc kat krextor llamapun mathhub mmt mws omdoc openmathmap sTeX sally smglom swim
bib.projects = FormalCAD jem latin logosphere mathsearch oaf odk odkWP6 omoc once-cs openmath-tn MaMoReD comma almanac frameit
bib.theses = phdthesis mscthesis bscthesis mscproject bscproject theses = $(bib.people) $(bib.projects) $( $(bib.theses)
# Sources
src = src/
bib.src = ./
ltxml.src = $(src)ltxml/
tex.src = $(src)tex/
html.src = $(src)html/
pubs.src = $(src)pubs/
# Destination
dist = dist/
bib.dist = ./kwarc.bib
ltxml.dist = $(dist)ltxml/
tex.dist = $(dist)tex/
html.dist = $(dist)html/
pubs.dist = $(dist)pubs/
# Scripts etc
bib.sty = $(ltxml.src)kwarcbibs.sty
html.script = $(html.src)generate-html
CRXSL = $(ltxml.src)crossrefs.xsl
PLXSL = $(pubs.src)publist.xsl
PLXSLA = $(pubs.src)publist-all.xsl
### </CONFIG> ###
# FOR kwarc.bib files = $(bib.all:%=$(bib.src)%)
# for kwarc.bib.xml files = $(bib.sty) $(bib.sty).ltxml
kwarc.ltxml.out = $(bib.ext:%=$(ltxml.dist)%.xml)
kcr.src = $(bib.kcr:%=$(bib.src)%) = $(ltxml.dist)kcr.bib
kcr.ltxml.out = $(
### TARGETS ###
all: dist
clean: clean-bib clean-xml clean-html clean-pubs
dist: bib xml pubs
# kwarc.bib --> concat files
bib: setup-bib $(bib.dist)
mkdir -p $(dist)
-rm $(bib.dist)
awk 'FNR==1{print ""}{print}' $( > $(bib.dist)
# *.bib.xml --> use latexmlc
xml: setup-xml $(kwarc.ltxml.out)
mkdir -p $(ltxml.dist)
-rm -r $(ltxml.dist)
$(kwarc.ltxml.out): $(ltxml.dist)%.xml: $(bib.src)% $(
latexmlc $< --quiet --bibtex --includestyles --path=$(ltxml.src) --preload=$(bib.sty).ltxml --destination=$@ 2> >(tee $@.ltxlog >&2)
# kcr.bib.xml --> use latexmlc after generating kcr.bib
$( $(kcr.src)
cat $(kcr.src) > $@
$(kcr.ltxml.out): $(
latexmlc $< --quiet --bibtex --includestyles --path=$(ltxml.src) --preload=$(bib.sty).ltxml --destination=pre-$@ 2> >(tee $@.ltxlog >&2)
xsltproc -o $@ $(CRXSL) pre-$@
rm -f pre-$@
# *.html --> custom script (xsltproc + latexml)
html: setup-html $(kcr.ltxml.out)
$(SHELL) $(html.script) $(src) $(dist) "$("
mkdir -p $(html.dist)
mkdir -p ${tex.dist}
mkdir -p $(ltxml.dist)
-rm -r $(html.dist)
-rm -r ${tex.dist}
# pubs --> xsltproc
pubs: setup-pubs html $( $(pubs.dist)/index.html
$(pubs.dist)/index.html: setup-pubs html
xsltproc --path $(html.dist) -o $(pubs.dist)/index.html $(PLXSLA) $(PLXSLA)
mkdir -p $(pubs.dist)
-rm -r $(pubs.dist)
$( %: $(PLXSL)
mkdir -p $(pubs.dist)$@
xsltproc --path $(html.dist) --stringparam id $@ -o $(pubs.dist)$@/index.html $(PLXSL) $(PLXSL)
######## testing
test: $(kcr.ltxml.out)
@echo $(kwarc.ltxml.out)
# The KWARC.bib repository [![Build Status](](
The repository contains the bib resources of the KWARC group, most notably the
citation database ```kwarc.bib```. It is generated automatically by concatenating
several source files via a [Travis CI]( build job.
We additionally use the Travis job to generate
[publication websites]( with the help of
[LaTeXML]( - see (far below).
## Using the KWARC bibs
In the simplest case, just clone the repository, and extend your ```BIBINPUTS```
environment variable so that it can find it. On a UNIX system something like the following
should work.
cd /path/to/your/setup
mkdir -p KWARC
git clone
echo 'export BIBINPUTS="${BIBINPUTS}:/path/to/your/setup/KWARC/bibs:"' >> ~/.bashrc
Your `BIBINPUTS` should look something like this: `".//:/path/to/your/setup/KWARC/bibs:"`.
Of course you will have to replace ```/path/to/your/setup``` with a path appropriate to
your system.
If you want to use the KWARC in a revision control system for a larger group, read (far) below.
## File structure
This repository contains two main folders: ```src/``` and ```dist/```. The first
folder contains the sources used to generate the content of the latter. All bib
files are toplevel.
## Bib files
The top-level bib files concatenated to create the unified ```kwarc.bib```
file. The sources are:
* ```preamble.bib``` – LaTeX preamble that defines shared macros and strings
* ```kwarcpubs.bib``` – individual publications of KWARC members (e.g. ```@article```, ```@inproceedings```)
* ```kwarccrossrefs.bib``` – crossref targets (e.g. ```@proceedings```) edited by KWARC
members (e.g. when one of us chaired a workshop)
* ```extpubs.bib``` – publications by external researchers (which may cross-reference
targets in ```kwarccrossrefs.bib```!)
* ```extcrossrefs.bib``` – crossref targets edited by external researchers,
regardless of whether KWARC or external publications refer to them.
* ```deprecated.bib``` deprecated citations that are still kept in ```kwarc.bib``` to
format old papers. NOTE that they may contain double crossrefs that need to be fixed
manually (the bib is mostly for documentation purposes), best by moving to the
non-deprecated versions.
For making citations in your documents, you can simply continue to use the
all-in-one ```kwarc.bib``` (but keep in mind that it is not editable!), or
alternatively you can use the individual files. In the latter case, use the
following order:
1. ```preamble.bib```
2. pubs.bib
3. crossrefs.bib
## Editing
The source files do not have any particular order.
Do not use any graphical frontend for editing, but use a text
editor, as the latter makes sure that changes are easy to spot
when using Git/Subversion's diff.
Do not touch anything that you don't understand.
It is easiest to create new entries by copying and modifying
existing ones.
## Online Publications
For online publications, it is strongly recommended to use
BibLaTeX's ```@online{foo:on}``` entries; see
Most online publications come in multiple variants for
compatibility with legacy publication workflows (such as LNCS).
The naming scheme is:
* ```@online{entry:on}``` -- BibLaTeX ```online``` entry
* ```@webpage{entry:webpage}``` -- alpha[h]url, an older solution for
online citations
* ```@misc{entry:web}``` -- plain BibTeX entry
* ```@misc{entry:base}``` -- crossref'd by the others above, contains
common fields, not suitable for citation
# Publication Pages
We use the Travis job to generate
[publication websites]( with the help of
[LaTeXML]( Additionally, we generate
specific publication pages for [KWARC members](,
[KWARC projects](, and theses. This behavior is triggered by
the `pubs` key in the bibTeX entries: an entry with `pubs = {foo,bar}` will be listed in
the publication pages and
## The Build Process
In a nutshell, the build process transforms `kwarcpubs.bib` and `kwarccrossrefs.bib` to LTXML format via
[LaTeXML]( Then we run the script `src/pubs/publist.xsl`
over it for all the values from the `pubs=` field in the bibTeX entries that are registered
in the `` variable in the `Makefile`. `publist.xsl`
selects the respective items and makes a html file from that. The results are committed to
[the `gh-pages` branch]( and are then hosted by GitHub.
For details see the top-level `Makefile`.
## Adding a Person or Project Page to the Publication Pages (Generation)
To add a person to the publication pages
1. update the `bib.people` or `bib.projects` variable in the top-level `Makefile` and add the username of the person or project to add
2. update the `<xsl:choose>` statement in `src/pubs/publist.xsl` to set the real name of
the person or project to be added.
Travis will re-build the web page (takes about 30 min), but you should probably test by
building locally first.
## Building locally
The website and concatenated files are generated and pushed automatically via
TRAVIS. For building locally we use a ```Makefile```. It has the following
* ```all = dist```
* ```dist = bib pubs```
* ```bib``` Takes the individual .bib files and concatenates them into ```kwarc.bib```
* ```xml``` Takes the individual .bib files and generates xml versions of them in ```dist/ltxml/*.bib.xml``` using ```latexml```. The generated files are ```.gitignore```d as users should not need them.
* ```html``` Takes the generated xml files from above and uses latexml and xslt to first generate .tex files in ```dist/tex/name-type.tex``` and then html files ```dist/html/name-type.html```. Both types are gitignored. Uses an adapted version of the ```generate-pubwww``` script, now found in ```src/html/generate.html```.
* ```pubs``` Takes the generated html files and builds a nice-looking bibliography in ```dist/pubs```. The output is .gitignored and intended to be committed to a gh-pages branch later on. Although that would still need an index.html, but that should not be a problem.
* ```clean-bib```, ```clean-xml```, ```clean-html```, ```clean-pubs```Removes files generated by an individual target.
* ```clean``` Removes **all** generated files
The ```xml``` and ```html``` targets depend on a working latexml installation. The ```html``` and ```pubs``` targets also need ```xsltproc```.
# Using this repo in a paper repository
We write most of our papers in ```git``` repositories, there it is usually a good idea to
make this repository into an external sub-repository that can be updated as necessary. In
the instructions below we assume that you - as the paper repos maintainer - want to add the
KWARC bibs as a sub-repository at path ```lib/kbibs``` from the top of the paper
## The best way for GIT
is via the ```git-subrepo``` extension of ```git```. Unfortunately this is not part of git
(yet). So you as the paper repos maintainer have to
[install it first]( if you want to
install the KWARC bibs as a subrepos. Your users do not, they will get the subrepos
automatically on ```git clone``` or ```git pull```.
1. go to the top of your paper prehistory: ```cd path/to/top``` (you can only make a
"subrepo" from there)
2. add the KWARC bibs repos as a "subrepo": ```git subrepo clone lib/kbibs```
Note that under ```git-subrepo``` the "external" is not updated automatically, a
maintainer has to "pull" it. This can be seen as a feature and not a bug (there is less of
a chance to break things).
1. go to the top of your paper repository: ```cd path/to/top``` (you can only pull from there)
2. pull the KWARC bibs repos as a "subrepo": ```git subrepo pull lib/kbibs```
To contribute changes back to the the KWARC bibs repository, you analogously do
1. go to the top of your paper prehistory: ```cd path/to/top``` (you can only push from there)
2. pull the KWARC bibs repos as a "subrepo": ```git subrepo push lib/kbibs```
## The second best way for GIT
is via ```git subtree```.
1. go to the top of your paper repository: ```cd path/to/top```
2. add the KWARC bibs repos as a remote: ```git remote add kbibs``` under the name ```kbibs```.
3. add the remote ```kbibs``` as a subtree: ```git subtree add --prefix=lib/kbibs kbibs master --squash```
(here under the path ```lib/kbibs```). The ```--squash``` reduces history noise.
When you want to update the subrepository to the newest version, you have to "subtree
pull" as above:
1. go to the top of your paper repository: ```cd path/to/top```
2. subtree-pull: ```git subtree pull --prefix=lib/kbibs kbibs master --squash```
this is a bit inconvenient, but works well.
Contributing back to the KWARC bibs repository is somewhat more complex; RTFM!
## Externals in SVN
In a subversion repository you can must make an external by
1. go to the top of your paper prehistory: ```cd path/to/top```
2. make the ```lib``` subdir if necessary: ```mkdir lib```
3. add the external: ```svn propedit svn:externals lib```
4. an editor will appear, add the line ```kbibs bibs```
5. commit your work: ```svn commit -m'adding external for the KWARC bibs'```
Note that in SVN any ```svn update``` will update the KWARC bibs in the external as well.
<!-- LocalWords: kwarc.bib kwarcpubs.bib kwarccrossrefs.bib crossref extpubs.bib foo:on
<!-- LocalWords: extcrossrefs.bib crossrefs entry:on entry:webpage entry:web entry:base
<!-- LocalWords: ltxml latexml gitignore xslt gitignored generate-pubwww gh-pages kbibs
<!-- LocalWords: xsltproc git-subrepo readme subrepos subrepos subrepo easypeasy subdir
<!-- LocalWords: subrepository svn:externals
## License
Licensed under CC0 1.0 Universal
title = {Search Interfaces for Mathematicians},
author = {Andrea Kohlhase},
crossref = {CICM14},
pages = {153--168},
url = {},
pubs = {akohlhase}}
editor = {Stephan Watt and James Davenport and Alan Sexton and Petr Sojka and Josef Urban},
venue = {Coimbra, Portugal},
eventdate = {2014-07-07/2014-07-11},
eventtitle = {Conferences on Intelligent Computer Mathematics},
title = {Intelligent Computer Mathematics},
booktitle = {{Intelligent Computer Mathematics} 2014},
NOkey = {CICM14},
NOlabel = {CICM14},
keywords = {conference},
publisher = {Springer},