Merge branch 'master' into 'master'

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

See merge request !1

WS2021/logrels/README.md

+# N. Roux: “A Beginner's Guide to Logical Relations for a Logical Framework”
+
+Based on [“Logical Relations for a Logical Framework”](https://kwarc.info/people/frabe/Research/RS_logrels_12.pdf) (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](https://uniformal.github.io/).
+
+- **Manuscript/Guide:** [./guide.pdf](./guide.pdf) (submitted 2021-03-22)
+- **Talk:** <https://www.youtube.com/watch?v=0rS3ol_J9Wo> (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/README.md`](./sources/README.md) for building.<br>
+(Note to core kwarc members: the sources are manually mirrored, hopefully consistently, at <https://gl.kwarc.info/supervision/roux_navid/-/tree/master/msc-seminar/slides-and-report>.)
+
+## 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”](https://kwarc.info/people/frabe/Research/RS_logrels_12.pdf) (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](https://uniformal.github.io/) 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.**

WS2021/logrels/sources/.gitignore

+creationdate.timestamp
+
+build/*
+!build/slides-logrel-pushout.pdf
+!build/slides.pdf
+!build/slides-with-notes.pdf
+!build/*[fF]inal*.pdf
+!build/*[sS]ubmitted*.pdf
+!build/*[pP]resented*.pdf
+
+# from the comments package
+**/comment.cut
+
+**/*.bbl
+**/*.blg
+**/*.aux
+**/*.bcf
+**/*.fdb_latexmk
+**/*.fls
+**/*.log
+**/*.out
+**/*.run.xml
+**/*.synctex.gz
+**/*.synctex(busy)
+**/*.tdo
+**/*.toc
+**/*.dvi
+**/*.xdv
+**/*.lox
+**/*.lof
+**/*.nav
+**/*.snm
+**/*.vrb
+**/*.pyg
+**/*.pygstyle
+
+~$*.pptx

WS2021/logrels/sources/.latexmkrc

+use Config;
+
+if (not exists $ENV{'TEXINPUTS'}) {
+	$ENV{'TEXINPUTS'} = '';
+}
+
+$ENV{'TEXINPUTS'} = $ENV{'TEXINPUTS'} . $Config{path_sep} . '..' . $Config{path_sep};
+
+# Use LuaLaTeX: https://tex.stackexchange.com/a/356432
+$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

WS2021/logrels/sources/README.md

+# 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 <https://gl.kwarc.info/supervision/seminar/-/tree/master/WS2021/logrels> (as `slides.pdf` and `guide.pdf`, respectively) and keep the sources there synced with the sources here.
\ No newline at end of file

WS2021/logrels/sources/bib/kwarc/.gitignore

+.DS_Store
+dist
+auto
+dist/ltxml
+dist/tex
+dist/html
+dist/pubs
+deploy_key

WS2021/logrels/sources/bib/kwarc/.gitrepo

+; 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 https://github.com/git-commands/git-subrepo#readme
+;
+[subrepo]
+	remote = git@github.com:KWARC/bibs.git
+	branch = master
+	commit = 7098dbecfefc25585680dfe04b6f4fb364649c84
+	parent = bea08dab19c3b2800b73b0fe2f34c3c789ddb6aa
+	method = merge
+	cmdver = 0.4.3

WS2021/logrels/sources/bib/kwarc/.travis.yml

+language: generic # don't install any environment
+os: linux
+dist: xenial
+
+script: /bin/bash src/travis/deploy.sh
+env:
+  global:
+  - ENCRYPTION_LABEL: "80dbef1467b0"
+  - COMMIT_AUTHOR_EMAIL: "45969094+kwarcbot@users.noreply.github.com"

WS2021/logrels/sources/bib/kwarc/LICENSE

+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
+<http://creativecommons.org/publicdomain/zero/1.0/>
+

WS2021/logrels/sources/bib/kwarc/Makefile

+SHELL:=/bin/bash
+
+### <CONFIG> ###
+# BIB files
+bib.cr				= kwarccrossrefs.bib extcrossrefs.bib
+bib.kcr 			= kwarcpubs.bib $(bib.cr)
+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
+bib.systems			= 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.do				= $(bib.people) $(bib.projects) $(bib.systems) $(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
+kwarc.bib.in		= $(bib.all:%=$(bib.src)%)
+
+# for kwarc.bib.xml files
+kwarc.ltxml.in		= $(bib.sty) $(bib.sty).ltxml
+kwarc.ltxml.out		= $(bib.ext:%=$(ltxml.dist)%.xml)
+kcr.src			= $(bib.kcr:%=$(bib.src)%)
+kcr.ltxml.in		= $(ltxml.dist)kcr.bib
+kcr.ltxml.out		= $(kcr.ltxml.in).xml
+
+### 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)
+setup-bib:
+	mkdir -p $(dist)
+clean-bib:
+	-rm $(bib.dist)
+$(bib.dist): 
+	awk 'FNR==1{print ""}{print}' $(kwarc.bib.in) > $(bib.dist)
+
+# *.bib.xml --> use latexmlc
+xml: setup-xml $(kwarc.ltxml.out)
+setup-xml:
+	mkdir -p $(ltxml.dist)
+clean-xml: 
+	-rm -r $(ltxml.dist)
+$(kwarc.ltxml.out): $(ltxml.dist)%.xml: $(bib.src)% $(kwarc.ltxml.in)
+	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.ltxml.in): $(kcr.src)
+	cat $(kcr.src) > $@
+$(kcr.ltxml.out): $(kcr.ltxml.in)
+	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) "$(bib.do)"
+setup-html:
+	mkdir -p $(html.dist)
+	mkdir -p ${tex.dist}
+	mkdir -p $(ltxml.dist)
+clean-html:
+	-rm -r $(html.dist)
+	-rm -r ${tex.dist}
+
+# pubs --> xsltproc
+pubs: setup-pubs html $(bib.do) $(pubs.dist)/index.html
+$(pubs.dist)/index.html: setup-pubs html
+	xsltproc --path $(html.dist) -o $(pubs.dist)/index.html $(PLXSLA) $(PLXSLA)
+setup-pubs:
+	mkdir -p $(pubs.dist)
+clean-pubs:
+	-rm -r $(pubs.dist)
+
+$(bib.do): %: $(PLXSL)
+	mkdir -p $(pubs.dist)$@
+	xsltproc --path $(html.dist) --stringparam id $@ -o $(pubs.dist)$@/index.html $(PLXSL) $(PLXSL)
+
+######## testing
+test: $(kcr.ltxml.out)
+
+echo:
+	@echo $(kwarc.ltxml.out)

WS2021/logrels/sources/bib/kwarc/README.md

+# The KWARC.bib repository [![Build Status](https://travis-ci.org/KWARC/bibs.svg?branch=master)](https://travis-ci.org/KWARC/bibs)
+
+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](https://travis-ci.org/) build job. 
+We additionally use the Travis job to generate  
+[publication websites](https://kwarc.github.io/bibs/) with the help of 
+[LaTeXML](http://dlmf.nist.gov/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
+cd KWARC
+git clone https://github.com/KWARC/bibs
+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 
+http://trac.kwarc.info/KWARC/wiki/BibLaTeX 
+ 
+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](https://kwarc.github.io/bibs/) with the help of
+[LaTeXML](http://dlmf.nist.gov/LaTeXML/).  Additionally, we generate
+specific publication pages for [KWARC members](http://kwarc.info/people/), 
+[KWARC projects](http://kwarc.info/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 http://kwarc.github.io/foo and http://kwarc.github.io/bar.
+
+## The Build Process
+In a nutshell,  the build process transforms `kwarcpubs.bib` and `kwarccrossrefs.bib` to LTXML format via
+[LaTeXML](http://dlmf.nist.gov/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 `bibs.do` 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](https://github.com/KWARC/bibs/tree/gh-pages) 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 
+targets: 
+
+* ```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
+repository.
+## 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](https://github.com/git-commands/git-subrepo#readme) 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 git@github.com:KWARC/bibs.git 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```
+
+easypeasy!
+
+## 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
+    git@github.com:KWARC/bibs.git``` 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 https://github.com/KWARC/bibs/trunk```
+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

WS2021/logrels/sources/bib/kwarc/ako.bib

+@inproceedings{Koh:SearchInterfacesMath:2014,
+  title = {Search Interfaces for Mathematicians},
+  author = {Andrea Kohlhase},
+  crossref = {CICM14},
+  pages = {153--168},
+  url = {http://arxiv.org/abs/1405.3758},
+  pubs = {akohlhase}}
+  
+  @proceedings{CICM14,
+  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},
+  series    = {LNCS},
+  number    = {8543},
+  isbn = {978-3-319-08433-6},
+  year = 2014,
+  acceptancerate = {64},
+  acceptancerateCOMMENT = {MKM/Calculemus/DML: 26/41, S&P: 9/14, overall: 35/55},
+}
+  
+  @INPROCEEDINGS{KohKoh:esmk05,
+  author = {Andrea Kohlhase and Michael Kohlhase},
+  title = {An Exploration in the Space of Mathematical Knowledge},
+  crossref = {MKM05},
+  pages = {17--32},
+  url = {http://kwarc.info/kohlhase/papers/mkm05.pdf},
+  keywords = {conference},
+  pubs = {akohlhase,mkohlhase}}
+
+@PROCEEDINGS{MKM05,
+  title = {Mathematical Knowledge Management, MKM'05},
+  year = {2006},
+  editor = {Michael Kohlhase},
+  number = {3863},
+  series = {LNAI},
+  publisher = {Springer Verlag},
+  booktitle = {Mathematical Knowledge Management, MKM'05},
+  keywords = {conference},
+  pubs= {mkohlhase}}
+
+
+@article{GrayTall_DualityAmbiguityFlexibility_1994,
+ ISSN = {00218251, 19452306},
+ URL = {http://www.jstor.org/stable/749505},
+ abstract = {In this paper we consider the duality between process and concept in mathematics, in particular, using the same symbolism to represent both a process (such as the addition of two numbers 3+2) and the product of that process (the sum 3+2). The ambiguity of notation allows the successful thinker the flexibility in thought to move between the process to carry out a mathematical task and the concept to be mentally manipulated as part of a wider mental schema. Symbolism that inherently represents the amalgam of process/concept ambiguity we call a "procept." We hypothesize that the successful mathematical thinker uses a mental structure that is manifest in the ability to think proceptually. We give empirical evidence from simple arithmetic to support the hypothesis that there is a qualitatively different kind of mathematical thought displayed by the more able thinker compared to that of the less able one. The less able are doing a more difficult form of mathematics, which eventually causes a divergence in performance between them and their more successful peers.},
+ author = {Eddie M. Gray, David O. Tall},
+ journal = {Journal for Research in Mathematics Education},
+ number = {2},
+ pages = {116-140},
+ publisher = {National Council of Teachers of Mathematics},
+ title = {Duality, Ambiguity, and Flexibility: A `Proceptual' View of Simple Arithmetic},
+ volume = {25},
+ year = {1994}
+}
+
+@Article{AlsaediEtAl_ExistenceAndGlobalBehavior_2015,
+    Author = {Ramzi {Alsaedi} and Habib {M\^aagli} and Noureddine {Zeddini}},
+    Title = {{Existence and global behavior of positive solution for semilinear problems with boundary blow-up.}},
+    FJournal = {{Journal of Mathematical Analysis and Applications}},
+    Journal = {{J. Math. Anal. Appl.}},
+    ISSN = {0022-247X},
+    Volume = {425},
+    Number = {2},
+    Pages = {818--826},
+    Year = {2015},
+    Publisher = {Elsevier, San Diego, CA},
+    Language = {English},
+    DOI = {10.1016/j.jmaa.2014.12.066},
+    MSC2010 = {35J61 35B09 35B40 35B44},
+    Zbl = {1312.35094}
+}
+
+@Article{Rayner_EyeMovementResearchOverview_1998,
+    Author = {Keith Rayner},
+    Title = {{Eye Movements in Reading and Information Processing: 20 Years of Research}},
+    Journal = {{Psychological Bulletin}},
+    Volume = 124,
+    Number = 3,
+    Pages = {372-422},
+    Year = 1998,
+    Publisher = {American Psychological Association, Inc.},
+    Language = {English},
+}
+
+@article{Arcavi_VisRepsInMath_2003,
+  journal = {Educational Studies in Mathematics},
+  year = {2003},
+  volume  = {52},
+  number = {3},
+  pages = {215--241},
+  title = {The role of visual representations in the learning of mathematics},
+  author = {Abraham Arcavi}}
+ 
+@TechReport{ChanYeung_MathExpRecognitionSurvey_1999,
+  author =      {Kam-Fai Chan and Dit-Yan Yeung},
+  title =      {Mathematical Expression Recognition: A Survey},
+  institution =  {The Hong Kong University of Science \& Technology},
+  year =      {1999},
+  type =      {Technical Report},
+  number =      {HKUST-CS99-04}}
+
+@inproceedings{KamaliTompa_RetrievingMathContent_2013,
+ author = {Kamali, Shahab and Tompa, Frank Wm.},
+ title = {Retrieving Documents with Mathematical Content},
+ pages = {353--362},
+ crossref = {SIGIR13},
+ numpages = {10}
+}
+% url = {http://doi.acm.org/10.1145/2484028.2484083},
+ %doi = {10.1145/2484028.2484083}
+
+@article{ZanibbiBlostein_MathExp_2012,
+ author = {Zanibbi, Richard and Blostein, Dorothea},
+ title = {Recognition and Retrieval of Mathematical Expressions},
+ journal = {International Jorunal Document Analysis and Recognition},
+ volume = {15},
+ number = {4},
+ month = dec,
+ year = {2012},
+ issn = {1433-2833},
+ pages = {331--357},
+ doi = {10.1007/s10032-011-0174-4},
+ publisher = {Springer-Verlag},
+ address = {Berlin, Heidelberg}}
+
+@InCollection{YangEtAl_ShapeFeaturesExtraction_2008,
+  author =      {Mingqiang Yang and Kidiyo Kpalma and Joseph Ronsin},
+  title =      {A Survey of Shape Feature Extraction Techniques},
+  booktitle =      {Pattern Recognition},
+  publisher = {IN-TECH},
+  year =      2008,
+  editor =      {Peng-Yeng Yin},
+  pages =      {43--90}}
+
+@inproceedings{AlvaroZanibbi_LayoutHandwrittenMath_2013,
+ author = {Alvaro, Francisco and Zanibbi, Richard},
+ title = {A Shape-based Layout Descriptor for Classifying Spatial Relationships in Handwritten Math},
+ crossref= {DOCENG13},
+ pages = {123--126},
+ numpages = {4},
+ url = {http://doi.acm.org/10.1145/2494266.2494315},
+ doi = {10.1145/2494266.2494315},
+ publisher = {ACM}
+}
+
+@proceedings{DOCENG13,
+  editor    = {Simone Marinai and Kim Marriott},
+ title = {Proceedings of the 2013 {ACM} Symposium on Document Engineering},
+ booktitle = {Proceedings of the 2013 {ACM} Symposium on Document Engineering},
+ year = {2013},
+ isbn = {978-1-4503-1789-4},
+ location = {Florence, Italy}}
+
+@proceedings{SIGIR13,
+  editor    = {Gareth J. F. Jones and
+               Paraic Sheridan and
+               Diane Kelly and
+               Maarten de Rijke and
+               Tetsuya Sakai},
+ title = {Proceedings of the 36th International ACM SIGIR Conference on Research and Development in Information Retrieval},
+ booktitle = {Proceedings of the 36th International ACM SIGIR Conference on Research and Development in Information Retrieval},
+ year = {2013},
+ isbn = {978-1-4503-2034-4},
+ location = {Dublin, Ireland},
+ publisher = {ACM},
+ address = {New York, NY, USA}}
+
+@Article{AndraEtAl_ReadingMathReps_2015,
+author="Andr{\'a}, Chiara
+and Lindstr{\"o}m, Paulina
+and Arzarello, Ferdinando
+and Holmqvist, Kenneth
+and Robutti, Ornella
+and Sabena, Cristina",
+title="Reading Mathematics Representations: AN Eye-Tracking Study",
+journal="International Journal of Science and Mathematics Education",
+year="2015",
+volume="13",
+number="2",
+pages="237--259",
+abstract="We use eye tracking as a method to examine how different mathematical representations of the same mathematical object are attended to by students. The results of this study show that there is a meaningful difference in the eye movements between formulas and graphs. This difference can be understood in terms of the cultural and social shaping of human perception, as well as in terms of differences between the symbolic and graphical registers.",
+issn="1573-1774",
+doi="10.1007/s10763-013-9484-y",
+}
+
+@incollection{Schnotz_TextPicComprehension_2005,
+  author = {Wolfgang Schnotz},
+  title = {An Integrated Model of Text and Picture Comprehension},
+  booktitle = {The Cambridge Handbook of Multimedia Learning},
+  editor={R. E. Mayer},
+  pages={49--69 (72--103)},
+  publisher = {Cambridge University Press},
+  year = {2005 (2014)}
+}
+
+@inproceedings{AntoniettEtAl_Metacognition_2008,
+ author = {Antonietti, Alessandro and Colombo, Barbara and Schnotz, Wolfgang and Moreno, Roxana and Marley, Scott and Helak, John and Fiore, Stephen M. and Cuevas, Haydee M. and Scielzo, Sandro},
+ title = {Metacognition in Understanding Multimedia Presentations},
+ booktitle = {Proceedings of the 8th International Conference on International Conference for the Learning Sciences - Volume 3},
+ series = {ICLS'08},
+ year = {2008},
+ location = {Utrecht, The Netherlands},
+ pages = {166--173},
+ numpages = {8},
+ url = {http://dl.acm.org/citation.cfm?id=1599936.1600014},
+ acmid = {1600014},
+ publisher = {International Society of the Learning Sciences},
+} 
+
+@incollection{BeitlichReiss_LesenMathBeweise_2014,
+  author = {Jana Beitlich and Kristina Reiss},
+  title = {Das Lesen mathematischer Beweise - Eine Eye Tracking Studie},
+  booktitle = {Beitr{\"a}ge zum Mathematikunterricht 2014},
+  editor={J. Roth and J. Ames},
+  pages={157--160},
+  publisher = {WTM-Verlag},
+  year = {2014}
+}
+
+@article{DBLP:journals/cogsci/Johnson-Laird80,
+  author    = {Philip N. Johnson{-}Laird},
+  title     = {Mental Models in Cognitive Science},
+  journal   = {Cognitive Science},
+  volume    = {4},
+  number    = {1},
+  pages     = {71--115},
+  year      = {1980},
+  doi       = {10.1207/s15516709cog0401_4},
+  timestamp = {Sun, 05 May 2013 18:38:22 +0200},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/cogsci/Johnson-Laird80},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+
+@article{HendersonEtAl_semanticEyeMovements_1999,
+  author    = {John M. Henderson and {Phillip A.} {Weeks Jr.} and Andrew Hollingworth},
+  title     = {The effects of semantic consistency on eye movements during complex scene viewing},
+  journal   = {Journal of Experimental Psychology: Human Perception and Performance},
+  volume    = {25},
+  number    = {1},
+  pages     = {210-228},
+  year      = {1999},
+  doi       = {10.1037/0096-1523.25.1.210}
+}
+
+@article{StrahlEtAl_Formelschreck_2010,
+	author = {Alexander Strahl and Julian Grobe and Rainer M{\"u}ller},
+	title = {Was schreckt bei Formeln ab?  - Untersuchung zur Darstellung von Formeln},
+	journal = {PhyDid B - Didaktik der Physik - Beitr{\"a}ge zur DPG-Fr{\"u}hjahrstagung},
+	volume = 0,
+	number = 0,
+	year = 2010,
+	keywords = {Formelverst{\"a}ndnis}
+}
+%	url = {http://phydid.physik.fu-berlin.de/index.php/phydid-b/article/view/169}
+
+@book{Freudenthal_DidacticalPhenomenologyOfMathematics_1983,
+  added-at = {2007-03-30T09:18:22.000+0200},
+  address = {Dordrecht},
+  author = {Freudenthal, Hans},
+  biburl = {http://www.bibsonomy.org/bibtex/2433549f421d821fdfb0419f8dc66ae7d/rmosvold},
+  citeulike-article-id = {489542},
+  howpublished = {Hardcover},
+  interhash = {5290897bf30f85908c37f88ae60e1cfc},
+  intrahash = {433549f421d821fdfb0419f8dc66ae7d},
+  isbn = {9027715351},
+  keywords = {MathematicsEducation mathematics},
+  month = {December},
+  priority = {2},
+  publisher = {Reidel},
+  timestamp = {2007-04-18T11:17:00.000+0200},
+  title = {Didactical Phenomenology of Mathematical Structures (Mathematics Education Library)},
+}
+
+@inproceedings{NielsenLandauer_ModelFindingUsabilityProblems_1993,
+ author = {Nielsen, Jakob and Landauer, Thomas K.},
+ title = {A Mathematical Model of the Finding of Usability Problems},
+ booktitle = {Proceedings of the INTERACT '93 and CHI '93 Conference on Human Factors in Computing Systems},
+ series = {CHI '93},
+ year = {1993},
+ isbn = {0-89791-575-5},
+ location = {Amsterdam, The Netherlands},
+ pages = {206--213},
+ numpages = {8},
+ url = {http://doi.acm.org/10.1145/169059.169166},
+ doi = {10.1145/169059.169166},
+ acmid = {169166},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {Poisson models, cost-benefit analysis, heuristic evaluation, iterative design, usability engineering, usability problems, user testing}
+} 
+
+@article{Cichy_ImageryAndPerception_2012,
+author = {Cichy, Radoslaw M. and Heinzle, Jakob and Haynes, John-Dylan},
+title = {Imagery and Perception Share Cortical Representations of Content and Location},
+journal = {Cerebral Cortex},
+volume = {22},
+number = {2},
+pages = {372},
+year = {2012}
+}
+%eprint = {/oup/backfile/Content_public/Journal/cercor/22/2/10.1093/cercor/bhr106/2/bhr106.pdf}
+
+@book{Tye_ImageryDebate_2000,
+  author = {Tye, Michael},
+  month = {March},
+  year={2000},
+  series={Representation and Mind series},
+  publisher = {MIT Press},
+  title = {The Imagery Debate},
+}

WS2021/logrels/sources/bib/kwarc/bibtweaks.sty

+\renewbibmacro*{event+venue+date}{}
+\renewbibmacro*{doi+eprint+url}{%
+  \iftoggle{bbx:doi}
+    {\printfield{doi}\iffieldundef{doi}{}{\clearfield{url}}}
+    {}%
+  \newunit\newblock
+  \iftoggle{bbx:eprint}
+    {\usebibmacro{eprint}}
+    {}%
+  \newunit\newblock
+  \iftoggle{bbx:url}
+    {\usebibmacro{url+urldate}}
+    {}}
+
+%  LocalWords:  renewbibmacro doi eprint iftoggle bbx printfield iffieldundef