Merge branch 'master' of gl.kwarc.info:KWARC/kwarc.info/www

courses/swuv.md

@@ -46,10 +46,10 @@ die Arbeitsgruppe einzusteigen (z.B. für eine Master-Arbeit oder Promotion).
 | 16. 12. 2020 | Jan Frederik Schaefer | Prototyping NLU Pipelines -- A Type-Theoretical Framework | Msc. thesis presentation ([slides](https://github.com/jfschaefer/slides/raw/master/2020/swuv-msc-presentation/slides.pdf), [thesis](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2020/Schaefer_Jan_Frederik.pdf))
 | 23. 12. 2020 | entfällt | |
 | 13. 01. 2021 | Christian Cerny | Term Generation in MMT | BSc. thesis presentation
-| 20. 01. 2021 | Markus Wich | Autoformalization of Mathematics |
-| 27. 01. 2021 | Navid Roux | Logical Relations |
+| 20. 01. 2021 | Markus Wich | Autoformalization of Mathematics | [slides](https://gl.kwarc.info/supervision/seminar/-/blob/master/WS2021/wich-slides.pdf)
+| 27. 01. 2021 | Navid Roux | Logical Relations for a Logical Framework | [slides](https://gl.kwarc.info/supervision/seminar/-/blob/master/WS2021/2021-01-27-roux-logical-relations.pdf), [underlying paper](https://kwarc.info/people/frabe/Research/RS_logrels_12.pdf)
 | 03. 02. 2021 | Sebastian Weber | TBD |
-| 10. 02. 2021 | | |
+| 10. 02. 2021 | Max Rapp | Sequent Calculi for Argumentation and/or Adaptive Logics|
 
 ##### Vortragsthemen
 
@@ -82,7 +82,7 @@ abonnieren!
 |Datum|Sprecher|Thema|Notiz|
 |-----|--------|-----|----|
 | 22. 04. 2020 | Rabe | Admin, Themenvergabe |
-| 22. 04. 2020 | Roux | Functorial Diagram Operators |
+| 22. 04. 2020 | Navid Roux | Functorial Diagram Operators |
 | 29. 04. 2020 | Kohlhase| Themenvergabe, Workshop-Vortrag|
 | 06. 05. 2020 | ---- | fällt aus|
 | 13. 05. 2020 | Benjamin Bösl| FrameIT: A Logic-Based Framework for Serious  Games |
@@ -114,7 +114,7 @@ abonnieren!
 | 18. 12. 2019 | Christoph Alt | Formula Search for the nLab| 
 |  8.  1. 2020 | ---  | no seminar | 
 | 15.  1. 2020 | Takuto Asakura (NII Tokyo) | Towards Grounding of Formulae in Mathematical Objects| 
-| 22.  1. 2020 | Navid Roux | Composition of programming languages | 
+| 22.  1. 2020 | Navid Roux | Composition of Programming Languages | 
 | 29.  1. 2020 | -- | no seminar | 
 |  5.  2. 2020 | -- | no seminar| 
 

events/GI2020/index.md

@@ -8,8 +8,10 @@ The 2020 joint annual meeting of the GI groups [Deduction Systems](https://fg-de
 
 It will be organized by [Sergey Goncharov](https://www8.cs.fau.de/sergey) and [Florian Rabe](https://kwarc.info/people/frabe/).
 
+The meeting will take place online on March 26.
+
 The meeting was originally planned to take place from 30.09.2020 to 02.10.2020.
 But after discussions among the speakers of the GI groups and the local organizers, we have decided to postpone the meeting due to the current COVID-19-related uncertainties.
 
-We are currently hoping to have the meeting after the winter semester, e.g., in Spring 2021.
+We are currently hoping to have an in-person meeting in autumn 2021.
 We are monitoring the situation regarding COVID-19 and post further updates here.

people/jbetzendahl.md

@@ -16,7 +16,7 @@ start_date: 2016-08
 ---
 
 ### Description
-Hi, my name is Jonas Betzendahl and I'm a PhD Student at KWARC.
+Hi, my name is Jonas Betzendahl, my pronouns are [they/he](http://pronoun.is/they?or=he), and I'm a PhD Student at KWARC.
 
 I finished my Master's degree at Bielefeld University with a thesis at KWARC about the transportation of the standard mathematics library of the IMPS theorem prover into OMDOC format and everything associated. You can find it [here](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2018/jbetzendahl/thesis_imps2omdoc.pdf).
 

people/nroux.md

@@ -18,17 +18,43 @@ website: https://navid-roux.netlify.app/
 ---
 ### Description  
 
-I am a Master student at [FAU Erlangen-Nürnberg](https://www.fau.eu/), where I previously completed my B.Sc. degree with a thesis on [*Refactoring of Theory Graphs in Knowledge Representation Systems*](https://navid-roux.netlify.app/post/bsc-thesis/).
+I am a Computer Science M.Sc. student with research interests in *knowledge representation and processing* of formal content
+such as foundations, logics, type theories, and math.
+My advisors are [Michael Kohlhase](https://kwarc.info/people/mkohlhase/) and [Florian Rabe](https://kwarc.info/people/frabe/)
 
-My primary interests lie in the field of *Mathematical Knowledge Management* (MKM), where I like to apply and extend existing formal methods, such as [KWARC's MMT system](https://kwarc.info/systems/mmt/), to facilitate formalization and reuse of knowledge. Moreover, I find parallels to software engineering fascinating: correctness, refactoring, and prototyping all have a very pragmatic side from a programmer's perspective as well as a formal side within the realm of MKM and theorem provers. Last but not least, both fields require good UX for programmers/formalizers, which led me to learning and caring about non-text-based programming languages by means of [projectional editing](https://martinfowler.com/bliki/ProjectionalEditing.html).
+So far I have completed my Bachelor's thesis on [*Refactoring of Theory Graphs in Knowledge Representation Systems*](https://navid-roux.netlify.app/post/bsc-thesis/),
+my Master's project on [*Structure-Preserving Diagram Operators*](https://gl.kwarc.info/supervision/projectarchive/-/blob/master/2020/Roux_Navid.pdf), and am currently working on extending the latter for my Master's thesis.
+Common to all three works is the idea to first identify annoyances when trying to represent a very concrete thing
+(e.g. getting a *concise* formalization of algebra)
+and to then develop scalable solutions that are as general as possible in the setting of the .
+The latter mostly happens in the [MMT system](https://kwarc.info/systems/mmt/) paired with the [Edinburgh Logical Framework](https://en.wikipedia.org/wiki/Logical_framework#LF).
 
 ### Current Work
 
-Besides my Master studies, currently I am working…
+Besides my Master's studies, currently I am working…
 
-- …on extending previous work on [diagram operators](https://kwarc.info/people/frabe/Research/RS_diagops_19.pdf), which allow taking a pre-existing formalization (as a diagram) and transforming it in useful ways to another diagram, e.g. to consistently *Abelianize* a formalization of general, non-Abelian universal algebra.
+- **Master's Thesis:** developing a framework of diagram operators, both in theory and in the [MMT system](https://kwarc.info/systems/mmt/), that allows operators to systematically transform/translate/annotate diagrams of formalizations.
+  
+  With such a framework, we can concisely specify operators that translate formalizations of extensional type theory to formalizations of intensional type theories, or formalizations of FOL to sorted FOL, …
 
-- …with other KWARCies in the [FrameIT project](https://UFrameIT.github.io/) on exploiting MKM techniques for serious educational games. See our latest paper submission [*FrameIT: Detangling Knowledge Management from Game Design in Serious Games*](http://kwarc.info/kohlhase/submit/cicm20-frameit.pdf).
+- **[FrameIT](https://uframeit.org)** (side project joined at kwarc): developing a prototype of a serious educational game that exploits knowledge management and logic features of the [MMT system](https://kwarc.info/systems/mmt/).
+
+  That way, we separate developing the 3D game mechanics from encoding and management of the serious game contents.
+  We formalize the latter in the MMT system and thus enable all the features that it already provides.
+  Checking whether a player-entered solution is correct? Amounts to typechecking.
+  Composing multiple serious game contents? Amounts to combination of formalizations.
+  Translating serious game contents from one world to another? Amounts to a pushout in the formalization.
+
+  See our paper [*FrameIT: Detangling Knowledge Management from Game Design in Serious Games*](http://kwarc.info/kohlhase/submit/cicm20-frameit.pdf).
+
+- **MMT ecosystem:** developing [tools](https://github.com/ComFreek/mmteditor) and [multiple syntax highlighters](https://github.com/ComFreek/mmtpygments) making one's life even more enjoyable with the MMT system.
+
+### Previous Work
+
+- **Master's Project:** [*Structure-Preserving Diagram Operators*](https://gl.kwarc.info/supervision/projectarchive/-/blob/master/2020/Roux_Navid.pdf)
+- **Bachelor's Thesis:** [*Refactoring of Theory Graphs in Knowledge Representation Systems*](https://navid-roux.netlify.app/post/bsc-thesis/)
+
+See [my personal website](https://navid-roux.netlify.app/) for Master's courses I have taken.
 
 ### Contact
 

projects/almanac.md

@@ -7,7 +7,7 @@ teaser: Decision situations require individuals and organizations to choose betw
 
 active: true
 start_date: 'January 2018'
-end_date: 'December 2020'
+end_date: 'August 2021'
 publink: auto
 
 people: 

projects/mdh.md

@@ -6,7 +6,7 @@ shorttitle: MDH
 teaser: A Collaboration Project with Ljubljana University
 
 start_date: 2020-01
-end_date: 2020-12
+end_date: 2021-12
 active: true
 
 
@@ -14,9 +14,11 @@ people:
     - mkohlhase
     - frabe
     - kbercic
+    - twiesing
 
 funding: DAAD
 program: Collaboration Grant
 logo: public/daad_logo.svg
 ---
-To Be Written
+Modern mathematical research increasingly depends on collaborative tools, computational environments, and online databases, and these are changing the way mathematical research is conducted and how it is turned into applications. For example, engineers now use mathematical tools to build and simulate physical models based on systems of differential equations with millions of variables, combining building blocks and algorithms taken from libraries shared all over the internet.
+The KWARC group at FAU Erlangen-Nürnberg and the group at Ljubljana University collaborate on the establishment of MathDataHub, a semantic portal for mathematical data sets. 
\ No newline at end of file

projects/oaf.md

@@ -5,7 +5,7 @@ title: "OAF: An Open Archive for Formalizations"
 shorttitle: OAF
 teaser: The OAF Project builds a theoretical framework for interoperability of theorem prover libraries and implements an information system that host and align multiple libraries in a joint semantic setting.
 
-active: true
+active: false
 start_date: '2014'
 end_date: 'June 2020'
 publink: auto
@@ -31,7 +31,7 @@ OAF was a DFG-funded research project running from 2014-2020 and headed by Micha
 and Florian Rabe originally at Jacobs University Bremen and later at FAU Erlangen-Nürnberg.
 It centered on the integration of formal mathematical libraries.
 
-Both the [original proposal](http://kwarc.info/kohlhase/projects/oaf.pdf) and the [final report](projects/oaf-report.pdf) are available.
+Both the [original proposal](http://kwarc.info/kohlhase/projects/oaf.pdf) and the [final report](../oaf-report.pdf) are available.
 
 Formal/symbolic systems and their libraries are non-interoperable because they are based
 on differing, mutually incompatible foundations (e.g., set theory, higher-order logic,