Compare revisions

21c1540e · 21c1540e · 21c1540e · 21c1540e · 21c1540e · 21c1540e
--- a/events/GILogicWorkshops/2021/zeume.pdf
+++ b/events/GILogicWorkshops/2021/zeume.pdf
--- a/events/GILogicWorkshops/2022/bruse.pdf
+++ b/events/GILogicWorkshops/2022/bruse.pdf
--- a/events/GILogicWorkshops/2022/cfp.txt
+++ b/events/GILogicWorkshops/2022/cfp.txt
+Joint Logic Workshop: Logic in Computer Science and Deduction Systems
+– 26. Jahrestagung FG LogInf und Workshop der FG DedSys –
+https://kwarc.info/events/GILogicWorkshops/index.html
+
+Online Workshop hosted by FAU University Erlangen-Nürnberg
+Friday, April 8, 2022, whole day event
+
+==========================
+= CALL FOR CONTRIBUTIONS =
+==========================
+
+== Overview ==
+
+The annual Workshop on Logic in Computer Science (Jahrestagung)
+is the prime activity of the Interest Group on Logic in Computer Science (FG LogInf)
+of the German Society of Informatics (Gesellschaft für Informatik, GI).
+Together with the Interest Group on Deduction Systems (FG DedSys) of the GI
+the Joint Logic Workshop fosters mutual exchange and aims at exploring synergies
+between both groups.
+
+The Joint Logic Workshop is a meeting with an informal and friendly atmosphere,
+where everyone (not only the German community) interested in the relevant topics
+can report on their work in an accessible setting.
+
+A special focus of the workshop is on young researchers and students,
+who are particularly encouraged to present their ongoing research
+projects to a wider audience. Another goal of the meeting is to stimulate
+networking effects and to foster collaborative research projects.
+
+Because of the ongoing pandemic situation the Joint Logic Workshop is organized
+as an online event. Organizational details are published on the event's website.
+
+
+== Invited speakers ==
+
+We plan to have 1-2 invited talks; details will follow soon.
+
+
+== Organization ==
+
+We welcome contributions on all theoretical, experimental and applied
+aspects of formal logic, reasoning and deduction.
+Accepted contributions are presented in a talk of approx. 15-30 minutes
+(depending on the overall number of accepted contributions), including
+discussion.
+
+The Joint Logic Workshop will also host the annual general assembly
+(Mitgliederversammlungen) of FG LogInf.
+
+The Joint Logic Workshop is kindly hosted by the Theoretical Computer Science
+and Knowledge Representation groups at University of Erlangen-Nürnberg (FAU)
+and organized by Sergey Goncharov and Florian Rabe.
+
+
+== Submission ==
+
+Submission is open to everybody interested in logic and/or deduction systems.
+
+Please submit an extended abstract (max. one page) of your contribution to
+both Olaf Beyersdorff <olaf.beyersdorff@uni-jena.de> and 
+Alexander Steen <alexander.steen@uni-greifswald.de.
+Submissions will be weakly reviewed to ensure topical fit.
+
+Submission deadline: March 21, 2022
+Notification:        March 25, 2022
+
+
+== Scientific Committee ==
+
+Olaf Beyersdorff, University of Jena
+Thomas Schneider, University of Bremen
+Claudia Schon, University of Koblenz
+Alexander Steen, University of Greifswald
+
--- a/events/GILogicWorkshops/2022/cfpart.txt
+++ b/events/GILogicWorkshops/2022/cfpart.txt
+Joint Logic Workshop: Logic in Computer Science and Deduction Systems
+– 26. Jahrestagung FG LogInf und 33. Jahrestreffen FG DedSys (Deduktionstreffen) –
+https://kwarc.info/events/GI2020/index.html
+
+Online Workshop hosted by FAU University Erlangen-Nürnberg
+Friday, March 26, 2021, whole day event
+
+==========================
+= CALL FOR PARTICIPATION =
+==========================
+
+== Overview ==
+
+The annual Workshop on Logic in Computer Science (Jahrestagung)
+and the annual meeting Deduktionstreffen are the prime activities of the
+Interest Group on Logic in Computer Science (FG LogInf) and the
+Interest Group on Deduction Systems (FG DedSys) of the
+German Society of Informatics (Gesellschaft für Informatik), respectively.
+This year, the activities will be organized as a Joint Logic Workshop in order
+to foster mutual exchange and to explore potential synergies.
+
+The Joint Logic Workshop is a meeting with an informal and friendly atmosphere,
+where everyone (not only the German community) interested in the relevant topics
+can report on their work in an accessible setting.
+
+Because of the ongoing pandemic situation the Joint Loic Workshop had to be cancelled
+in 2020 and is now organized as an online event.
+Organizational details are published on the event's website.
+
+== Program ==
+
+The workshop will feature invited talks by Ana Sokolova and Dov Gabbay and 11 contributed talks.
+
+The detailed program is available at https://kwarc.info/events/GI2020/index.html
+
+The Joint Logic Workshop will also host the annual general assemblies
+(Mitgliederversammlungen) of both special interest groups.
+
+== Registration ==
+
+Participation is free, but an informal registration is necessary at https://docs.google.com/forms/d/1hF5TgGreilNI6YYEI7b1PbMYNnmxqIgnSKWN6JMOJko
+
+== Scientific Committee ==
+
+Olaf Beyersdorff, University of Jena
+Thomas Schneider, University of Bremen
+Claudia Schon, University of Koblenz
+Alexander Steen, University of Luxembourg
+
+The Joint Logic Workshop is kindly hosted by the Theoretical Computer Science
+and Knowledge Representation groups at University of Erlangen-Nürnberg (FAU)
+and organized by Sergey Goncharov and Florian Rabe.
--- a/events/GILogicWorkshops/2022/heule.pdf
+++ b/events/GILogicWorkshops/2022/heule.pdf
--- a/events/GILogicWorkshops/2022/woerz.pdf
+++ b/events/GILogicWorkshops/2022/woerz.pdf
--- a/events/GILogicWorkshops/index.md
+++ b/events/GILogicWorkshops/index.md
+---
+layout: page
+title: GI Meeting Deduction and Logic
+---
+
+The 2020-2022 annual meetings of the GI groups [Deduction Systems](https://fg-dedsys.gi.de/) and [Logic in Computer Science](https://fg-loginf.gi.de/)
+(Gemeinsames Jahrestreffen der GI-Fachgruppen Deduktionssysteme und Logik in der Informatik) take place jointly in Erlangen.
+They are organized by [Sergey Goncharov](https://www8.cs.fau.de/sergey) and [Florian Rabe](https://kwarc.info/people/frabe/).
+
+In fact, due to COVID-19 pandemic, online meetings took place.
+An in-person meeting of Deduction Systems is planned for 2022 as a part of the KI conference.
+
+The 2021 meeting is [here](2021/index.html).
+
+### Program of the Spring 2022 Meeting
+
+The meeting will take place online on April 8.
+The call for contributions is [here](2022/cfp.txt).
+
+The program will consist of multiple sessions of zoom talks in the zoom room https://fau.zoom.us/j/63889416032.
+The program is as follows:
+
+* Session 1: 10:00 - 11:00 (chair: Claudia Schon)
+  * 10:00: Martin Suda, **Invited talk** Integrating Machine Learning into Saturation-based ATPs [slides (if any)](2022/suda.pdf)
+* Break 1: 11:00 - 11:30: free discussion in zoom
+* Session 2: 11:30 - 13:00 (chair: Florian Rabe)
+  * 11:30: Florian Wörz, Number of Variables for Graph Differentiation and the Resolution of GI Formulas [slides (if any)](2022/woerz.pdf)
+  * 12:00: Martin Lange, The Calculus of Influence - Formal Modelling of Biological Experiments [slides (if any)](2022/lange.pdf)
+  * 12:30: Florian Bruse, Model Checking Timed Recursive CTL, [slides (if any)](2022/bruse.pdf)
+* Lunch break: 13:00 - 14:00
+* Session 3: 14:00 - 15:30 (chair: Sergey Goncharov)
+  * 14:00: Colin Rothgang, Theorem Proving in Dependently Typed Higher-Order Logic [slides (if any)](2022/rothgang.pdf) 
+  * 14:30: Jean Christoph Jung and Frank Wolter, Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments [slides (if any)](2022/jung.pdf)
+  * 15:00: Hendrik Leidinger, SCL for First-Order Logic with Equality,  [slides (if any)](2022/lange.pdf)
+* Break 2: 15:30 - 16:00: free discussion in zoom
+* Session 4: 16:00 - 17:00 (chair: Olaf Beyersdorff)
+  * 16:00: Marijn Heule, **Invited talk** Short Proofs in Strong Proof Systems Fragments [slides (if any)](2022/heule.pdf)
+* Session 5: 17:15 - 18:00: Mitgliederversammlung Fachgruppe LogInf
--- a/events/Dubois.pdf
+++ b/events/Dubois.pdf
--- a/events/Gonthier.pptx
+++ b/events/Gonthier.pptx
--- a/events/Shankar.pdf
+++ b/events/Shankar.pdf
--- a/events/Smith.ppt
+++ b/events/Smith.ppt
--- a/events/Tetrapod2018/Thiery.pdf
+++ b/events/Tetrapod2018/Thiery.pdf
--- a/events/Tetrapod-2018.md
+++ b/events/Tetrapod-2018.md
@@ -42,7 +42,7 @@ Of particular interest are
 | Till Mossakowski  | Ontologies               |                        |
 | Natarajan Shankar | Proof Assistants         | [slides](Shankar.pdf)  |
 | Doug Smith        | Software Synthesis       | [slides](Smith.ppt)    |
-| Nicolas M. Thiery | Mathematical Computation | [slides](Thiery.html)  |
+| Nicolas M. Thiery | Mathematical Computation | [slides](Thiery.pdf)  |


 #### Organizers

--- a/events/Thiery.html
+++ b/events/Thiery.html
-<!DOCTYPE html>
-
-<html lang="en">
-
-<head>
-    <meta charset="utf-8">
-    <meta http-equiv="X-UA-Compatible" content="IE=edge">
-    <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=no">
-    <meta name="apple-mobile-web-app-capable" content="yes">
-    <meta name="apple-mobile-web-app-status-bar-style" content="black">
-    <meta name="mobile-web-app-capable" content="yes">
-    <title>
-        Modularity in Mathematical Computation - HackMD
-    </title>
-    <link rel="icon" type="image/png" href="https://hackmd.io/favicon.png">
-    <link rel="apple-touch-icon" href="https://hackmd.io/apple-touch-icon.png">
-
-    <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/twitter-bootstrap/3.3.7/css/bootstrap.min.css" integrity="sha256-916EbMg70RQy9LHiGkXzG8hSg9EdNy97GazNG/aiY1w=" crossorigin="anonymous" />
-    <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/4.7.0/css/font-awesome.min.css" integrity="sha256-eZrrJcwDc/3uDhsdt61sL2oOBY362qM3lon1gyExkL0=" crossorigin="anonymous" />
-    <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/ionicons/2.0.1/css/ionicons.min.css" integrity="sha256-3iu9jgsy9TpTwXKb7bNQzqWekRX7pPK+2OLj3R922fo=" crossorigin="anonymous" />
-    <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/octicons/3.5.0/octicons.min.css" integrity="sha256-QiWfLIsCT02Sdwkogf6YMiQlj4NE84MKkzEMkZnMGdg=" crossorigin="anonymous" />
-    <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/prism/1.5.1/themes/prism.min.css" integrity="sha256-vtR0hSWRc3Tb26iuN2oZHt3KRUomwTufNIf5/4oeCyg=" crossorigin="anonymous" />
-    <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.7.0/styles/github-gist.min.css" integrity="sha256-tAflq+ymku3Khs+I/WcAneIlafYgDiOQ9stIHH985Wo=" crossorigin="anonymous" />
-    <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/emojify.js/1.1.0/css/basic/emojify.min.css" integrity="sha256-UOrvMOsSDSrW6szVLe8ZDZezBxh5IoIfgTwdNDgTjiU=" crossorigin="anonymous" />
-    <style>
-        @import url(https://fonts.googleapis.com/css?family=Source+Sans+Pro:400,400italic,600,600italic,300italic,300|Source+Serif+Pro|Source+Code+Pro:400,300,500&subset=latin,latin-ext);.markdown-body{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Roboto,Helvetica,Arial,sans-serif;font-size:16px;line-height:1.5;word-wrap:break-word}.markdown-body:after,.markdown-body:before{display:table;content:""}.markdown-body:after{clear:both}.markdown-body>:first-child{margin-top:0!important}.markdown-body>:last-child{margin-bottom:0!important}.markdown-body a:not([href]){color:inherit;text-decoration:none}.markdown-body .absent{color:#c00}.markdown-body .anchor{float:left;padding-right:4px;margin-left:-20px;line-height:1}.markdown-body .anchor:focus{outline:none}.markdown-body blockquote,.markdown-body dl,.markdown-body ol,.markdown-body p,.markdown-body pre,.markdown-body table,.markdown-body ul{margin-top:0;margin-bottom:16px}.markdown-body hr{height:.25em;padding:0;margin:24px 0;background-color:#e7e7e7;border:0}.markdown-body blockquote{padding:0 1em;color:#777;border-left:.25em solid #ddd}.markdown-body blockquote>:first-child{margin-top:0}.markdown-body blockquote>:last-child{margin-bottom:0}.markdown-body .loweralpha{list-style-type:lower-alpha}.markdown-body h1,.markdown-body h2,.markdown-body h3,.markdown-body h4,.markdown-body h5,.markdown-body h6{margin-top:24px;margin-bottom:16px;font-weight:600;line-height:1.25}.markdown-body h1 .octicon-link,.markdown-body h2 .octicon-link,.markdown-body h3 .octicon-link,.markdown-body h4 .octicon-link,.markdown-body h5 .octicon-link,.markdown-body h6 .octicon-link{color:#000;vertical-align:middle;visibility:hidden}.markdown-body h1:hover .anchor,.markdown-body h2:hover .anchor,.markdown-body h3:hover .anchor,.markdown-body h4:hover .anchor,.markdown-body h5:hover .anchor,.markdown-body h6:hover .anchor{text-decoration:none}.markdown-body h1:hover .anchor .octicon-link,.markdown-body h2:hover .anchor .octicon-link,.markdown-body h3:hover .anchor .octicon-link,.markdown-body h4:hover .anchor .octicon-link,.markdown-body h5:hover .anchor .octicon-link,.markdown-body h6:hover .anchor .octicon-link{visibility:visible}.markdown-body h1 code,.markdown-body h1 tt,.markdown-body h2 code,.markdown-body h2 tt,.markdown-body h3 code,.markdown-body h3 tt,.markdown-body h4 code,.markdown-body h4 tt,.markdown-body h5 code,.markdown-body h5 tt,.markdown-body h6 code,.markdown-body h6 tt{font-size:inherit}.markdown-body h1{font-size:2em}.markdown-body h1,.markdown-body h2{padding-bottom:.3em;border-bottom:1px solid #eee}.markdown-body h2{font-size:1.5em}.markdown-body h3{font-size:1.25em}.markdown-body h4{font-size:1em}.markdown-body h5{font-size:.875em}.markdown-body h6{font-size:.85em;color:#777}.markdown-body ol,.markdown-body ul{padding-left:2em}.markdown-body ol.no-list,.markdown-body ul.no-list{padding:0;list-style-type:none}.markdown-body ol ol,.markdown-body ol ul,.markdown-body ul ol,.markdown-body ul ul{margin-top:0;margin-bottom:0}.markdown-body li>p{margin-top:16px}.markdown-body li+li{margin-top:.25em}.markdown-body dl{padding:0}.markdown-body dl dt{padding:0;margin-top:16px;font-size:1em;font-style:italic;font-weight:700}.markdown-body dl dd{padding:0 16px;margin-bottom:16px}.markdown-body table{display:block;width:100%;overflow:auto;word-break:normal;word-break:keep-all}.markdown-body table th{font-weight:700}.markdown-body table td,.markdown-body table th{padding:6px 13px;border:1px solid #ddd}.markdown-body table tr{background-color:#fff;border-top:1px solid #ccc}.markdown-body table tr:nth-child(2n){background-color:#f8f8f8}.markdown-body img{max-width:100%;box-sizing:content-box;background-color:#fff}.markdown-body img[align=right]{padding-left:20px}.markdown-body img[align=left]{padding-right:20px}.markdown-body .emoji{max-width:none;vertical-align:text-top;background-color:transparent}.markdown-body span.frame{display:block;overflow:hidden}.markdown-body span.frame>span{display:block;float:left;width:auto;padding:7px;margin:13px 0 0;overflow:hidden;border:1px solid #ddd}.markdown-body span.frame span img{display:block;float:left}.markdown-body span.frame span span{display:block;padding:5px 0 0;clear:both;color:#333}.markdown-body span.align-center{display:block;overflow:hidden;clear:both}.markdown-body span.align-center>span{display:block;margin:13px auto 0;overflow:hidden;text-align:center}.markdown-body span.align-center span img{margin:0 auto;text-align:center}.markdown-body span.align-right{display:block;overflow:hidden;clear:both}.markdown-body span.align-right>span{display:block;margin:13px 0 0;overflow:hidden;text-align:right}.markdown-body span.align-right span img{margin:0;text-align:right}.markdown-body span.float-left{display:block;float:left;margin-right:13px;overflow:hidden}.markdown-body span.float-left span{margin:13px 0 0}.markdown-body span.float-right{display:block;float:right;margin-left:13px;overflow:hidden}.markdown-body span.float-right>span{display:block;margin:13px auto 0;overflow:hidden;text-align:right}.markdown-body code,.markdown-body tt{padding:0;padding-top:.2em;padding-bottom:.2em;margin:0;font-size:85%;background-color:rgba(0,0,0,.04);border-radius:3px}.markdown-body code:after,.markdown-body code:before,.markdown-body tt:after,.markdown-body tt:before{letter-spacing:-.2em;content:"\A0"}.markdown-body code br,.markdown-body tt br{display:none}.markdown-body del code{text-decoration:inherit}.markdown-body pre{word-wrap:normal}.markdown-body pre>code{padding:0;margin:0;font-size:100%;word-break:normal;white-space:pre;background:transparent;border:0}.markdown-body .highlight{margin-bottom:16px}.markdown-body .highlight pre{margin-bottom:0;word-break:normal}.markdown-body .highlight pre,.markdown-body pre{padding:16px;overflow:auto;font-size:85%;line-height:1.45;background-color:#f7f7f7;border-radius:3px}.markdown-body pre code,.markdown-body pre tt{display:inline;max-width:auto;padding:0;margin:0;overflow:visible;line-height:inherit;word-wrap:normal;background-color:transparent;border:0}.markdown-body pre code:after,.markdown-body pre code:before,.markdown-body pre tt:after,.markdown-body pre tt:before{content:normal}.markdown-body .csv-data td,.markdown-body .csv-data th{padding:5px;overflow:hidden;font-size:12px;line-height:1;text-align:left;white-space:nowrap}.markdown-body .csv-data .blob-line-num{padding:10px 8px 9px;text-align:right;background:#fff;border:0}.markdown-body .csv-data tr{border-top:0}.markdown-body .csv-data th{font-weight:700;background:#f8f8f8;border-top:0}.markdown-body kbd{display:inline-block;padding:3px 5px;font-size:11px;line-height:10px;color:#555;vertical-align:middle;background-color:#fcfcfc;border:1px solid #ccc;border-bottom-color:#bbb;border-radius:3px;box-shadow:inset 0 -1px 0 #bbb}.news .alert .markdown-body blockquote{padding:0 0 0 40px;border:0 none}.activity-tab .news .alert .commits,.activity-tab .news .markdown-body blockquote{padding-left:0}.task-list-item{list-style-type:none}.task-list-item label{font-weight:400}.task-list-item.enabled label{cursor:pointer}.task-list-item+.task-list-item{margin-top:3px}.task-list-item-checkbox{float:left;margin:.31em 0 .2em -1.3em!important;vertical-align:middle;cursor:default!important}.markdown-body{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Roboto,Helvetica Neue,Helvetica,Arial,sans-serif;padding-top:40px;padding-bottom:40px;max-width:758px;overflow:visible!important}.markdown-body .emoji{vertical-align:top}.markdown-body pre{border:inherit!important}.markdown-body code{color:inherit!important}.markdown-body pre code .wrapper{display:-moz-inline-flex;display:-ms-inline-flex;display:-o-inline-flex;display:inline-flex}.markdown-body pre code .gutter{float:left;overflow:hidden;-webkit-user-select:none;user-select:none}.markdown-body pre code .gutter.linenumber{text-align:right;position:relative;display:inline-block;cursor:default;z-index:4;padding:0 8px 0 0;min-width:20px;box-sizing:content-box;color:#afafaf!important;border-right:3px solid #6ce26c!important}.markdown-body pre code .gutter.linenumber>span:before{content:attr(data-linenumber)}.markdown-body pre code .code{float:left;margin:0 0 0 16px}.markdown-body .gist .line-numbers{border-left:none;border-top:none;border-bottom:none}.markdown-body .gist .line-data{border:none}.markdown-body .gist table{border-spacing:0;border-collapse:inherit!important}.markdown-body code[data-gist-id]{background:none;padding:0}.markdown-body code[data-gist-id]:after,.markdown-body code[data-gist-id]:before{content:""}.markdown-body code[data-gist-id] .blob-num{border:unset}.markdown-body code[data-gist-id] table{overflow:unset;margin-bottom:unset}.markdown-body code[data-gist-id] table tr{background:unset}.markdown-body[dir=rtl] pre{direction:ltr}.markdown-body[dir=rtl] code{direction:ltr;unicode-bidi:embed}.markdown-body .alert>p{margin-bottom:0}.markdown-body pre.abc,.markdown-body pre.flow-chart,.markdown-body pre.graphviz,.markdown-body pre.mermaid,.markdown-body pre.sequence-diagram{text-align:center;background-color:inherit;border-radius:0;white-space:inherit}.markdown-body pre.abc>code,.markdown-body pre.flow-chart>code,.markdown-body pre.graphviz>code,.markdown-body pre.mermaid>code,.markdown-body pre.sequence-diagram>code{text-align:left}.markdown-body pre.abc>svg,.markdown-body pre.flow-chart>svg,.markdown-body pre.graphviz>svg,.markdown-body pre.mermaid>svg,.markdown-body pre.sequence-diagram>svg{max-width:100%;height:100%}.markdown-body pre>code.wrap{white-space:pre-wrap;white-space:-moz-pre-wrap;white-space:-pre-wrap;white-space:-o-pre-wrap;word-wrap:break-word}.markdown-body .alert>p,.markdown-body .alert>ul{margin-bottom:0}.markdown-body summary{display:list-item}.markdown-body summary:focus{outline:none}.markdown-body details summary{cursor:pointer}.markdown-body details:not([open])>:not(summary){display:none}.markdown-body figure{margin:1em 40px}.vimeo,.youtube{cursor:pointer;display:table;text-align:center;background-position:50%;background-repeat:no-repeat;background-size:contain;background-color:#000;overflow:hidden}.vimeo,.youtube{position:relative;width:100%}.youtube{padding-bottom:56.25%}.vimeo img{width:100%;object-fit:contain;z-index:0}.youtube img{object-fit:cover;z-index:0}.vimeo iframe,.youtube iframe,.youtube img{width:100%;height:100%;position:absolute;top:0;left:0}.vimeo iframe,.youtube iframe{vertical-align:middle;z-index:1}.vimeo .icon,.youtube .icon{position:absolute;height:auto;width:auto;top:50%;left:50%;transform:translate(-50%,-50%);color:#fff;opacity:.3;transition:opacity .2s;z-index:0}.vimeo:hover .icon,.youtube:hover .icon{opacity:.6;transition:opacity .2s}.slideshare .inner,.speakerdeck .inner{position:relative;width:100%}.slideshare .inner iframe,.speakerdeck .inner iframe{position:absolute;top:0;bottom:0;left:0;right:0;width:100%;height:100%}.MJX_Assistive_MathML{display:none}.ui-infobar{position:relative;z-index:2;max-width:758px;margin-top:25px;margin-bottom:-25px;color:#777}.ui-toc{position:fixed;bottom:20px;z-index:10000}.ui-toc-label{opacity:.3;background-color:#ccc;border:none;transition:opacity .2s}.ui-toc .open .ui-toc-label{opacity:1;color:#fff;transition:opacity .2s}.ui-toc-label:focus{opacity:.3;background-color:#ccc;color:#000}.ui-toc-label:hover{opacity:1;background-color:#ccc;transition:opacity .2s}.ui-toc-dropdown{margin-top:23px;margin-bottom:20px;padding-left:10px;padding-right:10px;max-width:45vw;width:25vw;max-height:70vh;overflow:auto;text-align:inherit}.ui-toc-dropdown>.toc{max-height:calc(70vh - 100px);overflow:auto}.ui-toc-dropdown[dir=rtl] .nav{padding-right:0;letter-spacing:.0029em}.ui-toc-dropdown a{overflow:hidden;text-overflow:ellipsis;white-space:pre}.ui-toc-dropdown .nav>li>a{display:block;padding:4px 20px;font-size:13px;font-weight:500;color:#767676}.ui-toc-dropdown .nav>li:first-child:last-child > ul,.ui-toc-dropdown .toc.expand ul{display:block}.ui-toc-dropdown .nav>li>a:focus,.ui-toc-dropdown .nav>li>a:hover{padding-left:19px;color:#000;text-decoration:none;background-color:transparent;border-left:1px solid #000}.ui-toc-dropdown[dir=rtl] .nav>li>a:focus,.ui-toc-dropdown[dir=rtl] .nav>li>a:hover{padding-right:19px;border-left:none;border-right:1px solid #000}.ui-toc-dropdown .nav>.active:focus>a,.ui-toc-dropdown .nav>.active:hover>a,.ui-toc-dropdown .nav>.active>a{padding-left:18px;font-weight:700;color:#000;background-color:transparent;border-left:2px solid #000}.ui-toc-dropdown[dir=rtl] .nav>.active:focus>a,.ui-toc-dropdown[dir=rtl] .nav>.active:hover>a,.ui-toc-dropdown[dir=rtl] .nav>.active>a{padding-right:18px;border-left:none;border-right:2px solid #000}.ui-toc-dropdown .nav .nav{display:none;padding-bottom:10px}.ui-toc-dropdown .nav>.active>ul{display:block}.ui-toc-dropdown .nav .nav>li>a{padding-top:1px;padding-bottom:1px;padding-left:30px;font-size:12px;font-weight:400}.ui-toc-dropdown[dir=rtl] .nav .nav>li>a{padding-right:30px}.ui-toc-dropdown .nav .nav>li>ul>li>a{padding-top:1px;padding-bottom:1px;padding-left:40px;font-size:12px;font-weight:400}.ui-toc-dropdown[dir=rtl] .nav .nav>li>ul>li>a{padding-right:40px}.ui-toc-dropdown .nav .nav>li>a:focus,.ui-toc-dropdown .nav .nav>li>a:hover{padding-left:29px}.ui-toc-dropdown[dir=rtl] .nav .nav>li>a:focus,.ui-toc-dropdown[dir=rtl] .nav .nav>li>a:hover{padding-right:29px}.ui-toc-dropdown .nav .nav>li>ul>li>a:focus,.ui-toc-dropdown .nav .nav>li>ul>li>a:hover{padding-left:39px}.ui-toc-dropdown[dir=rtl] .nav .nav>li>ul>li>a:focus,.ui-toc-dropdown[dir=rtl] .nav .nav>li>ul>li>a:hover{padding-right:39px}.ui-toc-dropdown .nav .nav>.active:focus>a,.ui-toc-dropdown .nav .nav>.active:hover>a,.ui-toc-dropdown .nav .nav>.active>a{padding-left:28px;font-weight:500}.ui-toc-dropdown[dir=rtl] .nav .nav>.active:focus>a,.ui-toc-dropdown[dir=rtl] .nav .nav>.active:hover>a,.ui-toc-dropdown[dir=rtl] .nav .nav>.active>a{padding-right:28px}.ui-toc-dropdown .nav .nav>.active>.nav>.active:focus>a,.ui-toc-dropdown .nav .nav>.active>.nav>.active:hover>a,.ui-toc-dropdown .nav .nav>.active>.nav>.active>a{padding-left:38px;font-weight:500}.ui-toc-dropdown[dir=rtl] .nav .nav>.active>.nav>.active:focus>a,.ui-toc-dropdown[dir=rtl] .nav .nav>.active>.nav>.active:hover>a,.ui-toc-dropdown[dir=rtl] .nav .nav>.active>.nav>.active>a{padding-right:38px}.markdown-body[lang^=ja]{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Roboto,Helvetica Neue,Helvetica,Arial,Hiragino Kaku Gothic Pro,\\30D2\30E9\30AE\30CE\89D2\30B4 Pro W3,Osaka,Meiryo,\\30E1\30A4\30EA\30AA,MS Gothic,"\FF2D\FF33   \30B4\30B7\30C3\30AF",sans-serif}.ui-toc-dropdown[lang^=ja]{font-family:Source Sans Pro,Helvetica,Arial,Meiryo UI,MS PGothic,"\FF2D\FF33   \FF30\30B4\30B7\30C3\30AF",sans-serif}.markdown-body[lang=zh-tw]{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Roboto,Helvetica Neue,Helvetica,Arial,PingFang TC,Microsoft JhengHei,\\5FAE\8EDF\6B63\9ED1,sans-serif}.ui-toc-dropdown[lang=zh-tw]{font-family:Source Sans Pro,Helvetica,Arial,Microsoft JhengHei UI,\\5FAE\8EDF\6B63\9ED1UI,sans-serif}.markdown-body[lang=zh-cn]{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Roboto,Helvetica Neue,Helvetica,Arial,PingFang SC,Microsoft YaHei,\\5FAE\8F6F\96C5\9ED1,sans-serif}.ui-toc-dropdown[lang=zh-cn]{font-family:Source Sans Pro,Helvetica,Arial,Microsoft YaHei UI,\\5FAE\8F6F\96C5\9ED1UI,sans-serif}.ui-affix-toc{position:fixed;top:0;max-width:15vw;max-height:70vh;overflow:auto}.back-to-top,.expand-toggle,.go-to-bottom{display:block;padding:4px 10px;margin-top:10px;margin-left:10px;font-size:12px;font-weight:500;color:#999}.back-to-top:focus,.back-to-top:hover,.expand-toggle:focus,.expand-toggle:hover,.go-to-bottom:focus,.go-to-bottom:hover{color:#563d7c;text-decoration:none}.back-to-top,.go-to-bottom{margin-top:0}.ui-user-icon{width:20px;height:20px;display:block;border-radius:3px;margin-top:2px;margin-bottom:2px;margin-right:5px;background-position:50%;background-repeat:no-repeat;background-size:contain}.ui-user-icon.small{width:18px;height:18px;display:inline-block;vertical-align:middle;margin:0 0 .2em}.ui-infobar>small>span{line-height:22px}.ui-infobar>small .dropdown{display:inline-block}.ui-infobar>small .dropdown a:focus,.ui-infobar>small .dropdown a:hover{text-decoration:none}.unselectable{-moz-user-select:none;-webkit-user-select:none;-o-user-select:none;user-select:none}@media print{blockquote,div,img,pre,table{page-break-inside:avoid!important}a[href]:after{font-size:12px!important}}.markdown-body.slides{position:relative;z-index:1;color:#222}.markdown-body.slides:before{content:"";display:block;position:absolute;top:0;left:0;right:0;bottom:0;z-index:-1;background-color:currentColor;box-shadow:0 0 0 50vw}.markdown-body.slides section[data-markdown]{position:relative;margin-bottom:1.5em;background-color:#fff;text-align:center}.markdown-body.slides section[data-markdown] code{text-align:left}.markdown-body.slides section[data-markdown]:before{content:"";display:block;padding-bottom:56.23%}.markdown-body.slides section[data-markdown]>div:first-child{position:absolute;top:50%;left:1em;right:1em;transform:translateY(-50%);max-height:100%;overflow:hidden}.markdown-body.slides section[data-markdown]>ul{display:inline-block}.markdown-body.slides>section>section+section:after{content:"";position:absolute;top:-1.5em;right:1em;height:1.5em;border:3px solid #777}body{font-smoothing:subpixel-antialiased!important;-webkit-font-smoothing:subpixel-antialiased!important;-moz-osx-font-smoothing:auto!important;text-shadow:0 0 1em transparent,1px 1px 1.2px rgba(0,0,0,.004);-webkit-overflow-scrolling:touch;font-family:Source Sans Pro,Helvetica,Arial,sans-serif;letter-spacing:.025em}.focus,:focus{outline:none!important}::-moz-focus-inner{border:0!important}body.modal-open{overflow-y:auto;padding-right:0!important}
-    </style>
-    <!-- HTML5 shim and Respond.js for IE8 support of HTML5 elements and media queries -->
-    <!-- WARNING: Respond.js doesn't work if you view the page via file:// -->
-    <!--[if lt IE 9]>
-    	<script src="https://cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv.min.js" integrity="sha256-3Jy/GbSLrg0o9y5Z5n1uw0qxZECH7C6OQpVBgNFYa0g=" crossorigin="anonymous"></script>
-    	<script src="https://cdnjs.cloudflare.com/ajax/libs/respond.js/1.4.2/respond.min.js" integrity="sha256-g6iAfvZp+nDQ2TdTR/VVKJf3bGro4ub5fvWSWVRi2NE=" crossorigin="anonymous"></script>
-		<script src="https://cdnjs.cloudflare.com/ajax/libs/es5-shim/4.5.9/es5-shim.min.js" integrity="sha256-8E4Is26QH0bD52WoQpcB+R/tcWQtpzlCojrybUd7Mxo=" crossorigin="anonymous"></script>
-    <![endif]-->
-</head>
-
-<body>
-    <div id="doc" class="markdown-body container-fluid"><h1 id="Modularity-in-Mathematical-Computation" style=""><a class="anchor hidden-xs" href="#Modularity-in-Mathematical-Computation" title="Modularity-in-Mathematical-Computation"><span class="octicon octicon-link"></span></a>Modularity in Mathematical Computation</h1><p>Nicolas M. Thiéry et al.</p><p>Tetrapod: Modular Knowledge workshop</p><p>FLoC 2018, Oxford, July 13th of 2018</p><h2 id="A-collaborative-document" style=""><a class="anchor hidden-xs" href="#A-collaborative-document" title="A-collaborative-document"><span class="octicon octicon-link"></span></a>A collaborative document</h2><p><strong>Please connect to:</strong></p><p><a href="https://tinyurl.com/tetrapod-2018-computation" target="_blank">https://tinyurl.com/tetrapod-2018-computation</a></p><hr><h2 id="Participants" style=""><a class="anchor hidden-xs" href="#Participants" title="Participants"><span class="octicon octicon-link"></span></a>Participants</h2><ul>
-<li>Georges Gonthier (Inria Saclay)</li>
-<li>Florian Rabe (FAU Erlangen-Nürnberg, LRI, Univ. Paris Sud)</li>
-<li>Dennis Müller (FAU Erlangen-Nürnberg)</li>
-<li>Jeremy Gibbons (University of Oxford), local observer and gate-crasher</li>
-<li>Jacques Carette (McMaster University) System designer and developper</li>
-<li>Nicolas M. Thiéry (LRI, Univ. Paris Sud) Practionner, SageMath dev</li>
-</ul><hr><h2 id="Abstract" style=""><a class="anchor hidden-xs" href="#Abstract" title="Abstract"><span class="octicon octicon-link"></span></a>Abstract</h2><p>Over the last decades, a huge amount of computational software was
-developed for pure mathematics, in particular to support research and
-education. As for any complex ecosystem of software components, the
-ability to compose them has a multiplier effect on the expressive
-power, flexibility, and range of applications.</p><p>The purpose of this session is to share experience on the many
-barriers to composability in computational mathematics, and how they
-are being tackled in various communities. Of particular interest will
-be the exploitation of knowledge to leverage some of the barriers.
-feedback from neighbor fields (proofs, data, knowledge) will be most
-welcome.</p><hr><h2 id="Composability" style=""><a class="anchor hidden-xs" href="#Composability" title="Composability"><span class="octicon octicon-link"></span></a>Composability?</h2><p>For this session we focus on the ability to transfer data
-and run procedures across “systems” (two different software, two instances of the same software on different machines, two libraries within a system, …).</p><hr><h3 id="Data-transfers" style=""><a class="anchor hidden-xs" href="#Data-transfers" title="Data-transfers"><span class="octicon octicon-link"></span></a>Data transfers</h3><ul>
-<li>
-<p><strong>Goal</strong>: Transfer an object O from system <code>A</code> to system <code>B</code></p>
-</li>
-<li>
-<p><strong>Requirements</strong>:</p>
-<ul>
-<li>
-<p><strong>A communication channel</strong>: shared memory, disk, pipe, (web)socket, …</p>
-</li>
-<li>
-<p><strong>A communication protocol</strong></p>
-</li>
-<li>
-<p><strong>Serialization / Deserialization</strong>: conversion to/from a string of bytes</p>
-</li>
-<li>
-<p><strong>A format specification</strong>; e.g. XML (syntax) + OpenMath content dictionary (semantic)</p>
-</li>
-<li>
-<p><strong>Format conversion</strong></p>
-<ul>
-<li>
-<p><strong>syntax</strong>: e.g.: JSON  &lt;-&gt;  XML</p>
-</li>
-<li>
-<p><strong>adaptation</strong>: <code>DihedralGroup(4)</code> &lt;-&gt; <code>DihedralGroup(8)</code></p>
-</li>
-<li>
-<p><strong>change of representation (codec)</strong>: recursive &lt;-&gt; sparse polynomial</p>
-</li>
-</ul>
-<p>Idealy: applying a theory morphism to guarantee semantic preservation</p>
-</li>
-</ul>
-</li>
-</ul><hr><h3 id="Procedure-calls" style=""><a class="anchor hidden-xs" href="#Procedure-calls" title="Procedure-calls"><span class="octicon octicon-link"></span></a>Procedure calls</h3><ul>
-<li>
-<p><strong>Goal</strong>: From <code>B</code> request the computation <code>f(a,b,c)</code> in <code>A</code></p>
-</li>
-<li>
-<p><strong>Requirements</strong>:</p>
-<ul>
-<li>
-<p><strong>Data transfers</strong>: send <code>a</code>,<code>b</code>,<code>c</code> to <code>A</code>, receive back the result</p>
-</li>
-<li>
-<p><strong>Procedure call</strong>: bindings, remote procedure calls, …</p>
-</li>
-<li>
-<p><strong>An API specification</strong>: syntax and semantic of <code>f</code> in <code>A</code>?</p>
-</li>
-<li>
-<p><strong>Adapting the API in B to the API in A</strong>: <code>Size(A)</code> &lt;-&gt; <code>A.cardinality()</code></p>
-<p>Idealy: applying a theory morphism to guarantee semantic preservation</p>
-</li>
-</ul>
-</li>
-</ul><hr><h2 id="Barriers-faced-by-the-computational-pure-maths-community" style=""><a class="anchor hidden-xs" href="#Barriers-faced-by-the-computational-pure-maths-community" title="Barriers-faced-by-the-computational-pure-maths-community"><span class="octicon octicon-link"></span></a>Barriers faced by the computational pure maths community?</h2><hr><h3 id="Semantic-barriers" style=""><a class="anchor hidden-xs" href="#Semantic-barriers" title="Semantic-barriers"><span class="octicon octicon-link"></span></a>Semantic barriers</h3><ul>
-<li>
-<p><strong>Many kinds of objects</strong>:</p>
-<p>E.g. thousands in Sage, compared to “matrices of floats” in Matlab</p>
-</li>
-<li>
-<p><strong>Many data representations</strong>, with very different algorithmic complexity</p>
-<p>E.g. for polynomials: sparse, dense, recursive, straight line
-program, evaluation, …</p>
-</li>
-<li>
-<p>Objects at different levels of abstraction</p>
-</li>
-<li>
-<p><strong>Few core concepts</strong></p>
-<p>addition, multiplication commutativity</p>
-</li>
-<li>
-<p>… but <strong>many interesting ways to combine them</strong>:</p>
-<p>Groups, Fields, graded commutative algebras, …</p>
-</li>
-<li>
-<p>A <strong>large variety of use cases</strong></p>
-<p>speed maniacs, flexibility fans, composability devouts</p>
-</li>
-</ul><hr><h4 id="The-good-news"><a class="anchor hidden-xs" href="#The-good-news" title="The-good-news"><span class="octicon octicon-link"></span></a>The good news</h4><ul>
-<li>
-<p>Formal level: <strong>best effort is ok</strong></p>
-</li>
-<li>
-<p>No requirements to define the maths behind</p>
-</li>
-</ul><hr><h3 id="Social-barriers" style=""><a class="anchor hidden-xs" href="#Social-barriers" title="Social-barriers"><span class="octicon octicon-link"></span></a>Social barriers</h3><ul>
-<li>
-<p><strong>Closed science</strong> and the <strong>Montaigu-Capulet syndrome</strong></p>
-<p>(won’t use code from / share code with XXX for political reasons)</p>
-</li>
-<li>
-<p><strong>Tight man power resources</strong></p>
-<p>Severel hundreds of thousands use computer algebra; hundreds implement it; a handful are
-officially paid full time for it.</p>
-</li>
-<li>
-<p><strong>Mastering math &amp; computer science</strong>?</p>
-</li>
-<li>
-<p><strong>High level of math specialization required when writing code</strong></p>
-<p>E.g. thousands of people use Gröbner bases; a handful know how to
-implement them right</p>
-</li>
-<li>
-<p>Pieces of software that took decades to develop</p>
-<p>We can’t afford to reimplement them; yet we can’t afford to not reimplement them (to learn from one’s mistakes and benefit from technology advances!)</p>
-</li>
-<li>
-<p>A fragmented community</p>
-</li>
-</ul><hr><h3 id="Technical-barriers" style=""><a class="anchor hidden-xs" href="#Technical-barriers" title="Technical-barriers"><span class="octicon octicon-link"></span></a>Technical barriers</h3><ul>
-<li>
-<p><strong>Systems written in different languages / idioms</strong></p>
-<p>C, C++, Python 2/3, Java, Javascript, Julia, GAP, Singular,
-Macaulay, Maple, Mathematica, MuPAD, Magma, Axiom/Aldor, Haskell, ML, Agda, …</p>
-</li>
-<li>
-<p><strong>Systems written using different frameworks / API</strong></p>
-</li>
-<li>
-<p><strong>Packaging barriers</strong></p>
-</li>
-<li>
-<p>Tendency for <strong>large old systems</strong>: 10-30 years, <span class="mathjax"><span class="MathJax_Preview" style="color: inherit; display: none;"></span><span class="MathJax" id="MathJax-Element-1-Frame" tabindex="0" style="position: relative;" data-mathml="<math xmlns=&quot;http://www.w3.org/1998/Math/MathML&quot;><msup><mn>10</mn><mn>6</mn></msup></math>" role="presentation"><nobr aria-hidden="true"><span class="math" id="MathJax-Span-1" style="width: 1.727em; display: inline-block;"><span style="display: inline-block; position: relative; width: 1.455em; height: 0px; font-size: 116%;"><span style="position: absolute; clip: rect(1.399em, 1001.46em, 2.608em, -1000em); top: -2.425em; left: 0em;"><span class="mrow" id="MathJax-Span-2"><span class="msubsup" id="MathJax-Span-3"><span style="display: inline-block; position: relative; width: 1.429em; height: 0px;"><span style="position: absolute; clip: rect(3.159em, 1000.96em, 4.171em, -1000em); top: -3.987em; left: 0em;"><span class="mn" id="MathJax-Span-4" style="font-family: MathJax_Main;">10</span><span style="display: inline-block; width: 0px; height: 3.987em;"></span></span><span style="position: absolute; top: -4.38em; left: 1em;"><span class="mn" id="MathJax-Span-5" style="font-size: 70.7%; font-family: MathJax_Main;">6</span><span style="display: inline-block; width: 0px; height: 3.987em;"></span></span></span></span></span><span style="display: inline-block; width: 0px; height: 2.425em;"></span></span></span><span style="display: inline-block; overflow: hidden; vertical-align: -0.088em; border-left: 0px solid; width: 0px; height: 1.153em;"></span></span></nobr><span class="MJX_Assistive_MathML" role="presentation"><math xmlns="http://www.w3.org/1998/Math/MathML"><msup><mn>10</mn><mn>6</mn></msup></math></span></span><script type="math/tex" id="MathJax-Element-1">10^6</script></span> lines of code</p>
-<ul>
-<li>
-<p>lots of <strong>technical debt</strong>; <strong>slow evolution</strong></p>
-</li>
-<li>
-<p><strong>Lack of modularity</strong>, <strong>large dependencies</strong></p>
-<p>E.g. having to install SageMath to use just a few of its lines</p>
-</li>
-</ul>
-</li>
-</ul><hr><h2 id="Some-case-studies-and-tentative-solutions" style=""><a class="anchor hidden-xs" href="#Some-case-studies-and-tentative-solutions" title="Some-case-studies-and-tentative-solutions"><span class="octicon octicon-link"></span></a>Some case studies and tentative solutions</h2><hr><h3 id="OpenMath" style=""><a class="anchor hidden-xs" href="#OpenMath" title="OpenMath"><span class="octicon octicon-link"></span></a>OpenMath</h3><ul>
-<li>
-<p><strong>Goal</strong>: standardized serialization format to exchange data across systems</p>
-</li>
-<li>
-<p><strong>Syntax</strong>: XML, json, binary</p>
-</li>
-<li>
-<p><strong>Semantic</strong>: defined by content dictionaries (CD)</p>
-</li>
-<li>
-<p><strong>Hard problem</strong>: agreeing on CD’s for polynomials was already hard; scaling?</p>
-</li>
-</ul><p>After twenty years, little adoption</p><hr><h3 id="The-Math-in-the-Middle-approach" style=""><a class="anchor hidden-xs" href="#The-Math-in-the-Middle-approach" title="The-Math-in-the-Middle-approach"><span class="octicon octicon-link"></span></a>The Math-in-the-Middle approach</h3><ul>
-<li>
-<p><strong>Goals</strong>:</p>
-<ul>
-<li>
-<p>Separate <strong>serialization</strong> from <strong>adaptation</strong></p>
-</li>
-<li>
-<p>Separate <strong>binding</strong> from <strong>adaptation</strong></p>
-</li>
-<li>
-<p>Separate the treatment of each system</p>
-</li>
-</ul>
-</li>
-<li>
-<p><strong>Approach</strong>:</p>
-<ul>
-<li>
-<p>A central math ontology</p>
-</li>
-<li>
-<p>Formalize each systems by aligning to the central ontology</p>
-</li>
-</ul>
-</li>
-</ul><hr><h3 id="Categories-in-GAP-Axiom-MuPAD-SageMath" style=""><a class="anchor hidden-xs" href="#Categories-in-GAP-Axiom-MuPAD-SageMath" title="Categories-in-GAP-Axiom-MuPAD-SageMath"><span class="octicon octicon-link"></span></a>Categories in GAP, Axiom, MuPAD, SageMath</h3><ul>
-<li>
-<p><strong>Barrier</strong>: compose building blocks <code>A1</code> and <code>A2</code> into modular generic code <code>B</code>: <code>f(a1, a2)</code></p>
-</li>
-<li>
-<p><strong>Requirements</strong>: <strong>uniform modular API</strong> + <strong>method resolution mechanism</strong></p>
-<p>Remember: few core concepts, hundreds of interesting combinations</p>
-</li>
-<li>
-<p><strong>Approaches</strong>:</p>
-<ul>
-<li>
-<p>Axiom, MuPAD: OOP with large hierarchies of abstract classes (categories)</p>
-</li>
-<li>
-<p>SageMath:</p>
-<ul>
-<li>same, but even larger</li>
-<li>based on standard OOP (Python) + infrastructure to scale</li>
-<li>embed semantic knowledge at single point of truth;
-exploit it to automatically generate the class hierarchy</li>
-</ul>
-</li>
-<li>
-<p>GAP: bespoke method resolution mechanism</p>
-</li>
-</ul>
-</li>
-</ul><hr><h3 id="Case-Study-libsemigroups-a-library-for-computing-with-semigroups" style=""><a class="anchor hidden-xs" href="#Case-Study-libsemigroups-a-library-for-computing-with-semigroups" title="Case-Study-libsemigroups-a-library-for-computing-with-semigroups"><span class="octicon octicon-link"></span></a>Case Study: libsemigroups:, a library for computing with semigroups</h3><p>Author: James B. Mitchel et al.</p><ul>
-<li>
-<p><strong>Problems</strong></p>
-<ul>
-<li>
-<p>Speeding GAP’s semigroup package while increasing its availability</p>
-</li>
-<li>
-<p>Use a low-level library <code>A</code> from a system <code>B</code> written in a different language</p>
-</li>
-</ul>
-</li>
-<li>
-<p><strong>Approach</strong></p>
-<ul>
-<li>
-<p>Rewrite as a standalone templated C++ library</p>
-</li>
-<li>
-<p>API: many iterations until converging to a natural API (no memory management, …)</p>
-</li>
-<li>
-<p>Bindings: from Python: on-the-fly binding using cppyy (also tried Cython, Pybind11, …)</p>
-</li>
-<li>
-<p>Adaptation: a thin layer for now; could use alignments</p>
-</li>
-</ul>
-</li>
-</ul><hr><h3 id="Case-Study-the-Sage--GAP-interface" style=""><a class="anchor hidden-xs" href="#Case-Study-the-Sage--GAP-interface" title="Case-Study-the-Sage--GAP-interface"><span class="octicon octicon-link"></span></a>Case Study: the Sage / GAP interface</h3><ul>
-<li>
-<p><strong>Problem</strong></p>
-<p>Use funtionalities from a system <code>A</code> in a system <code>B</code> written in a different language</p>
-</li>
-<li>
-<p><strong>Data exchange</strong></p>
-<ul>
-<li>
-<p>Objects returned as references (handles):</p>
-<ul>
-<li>Few conversions</li>
-<li>Reduced overhead</li>
-<li>Manipulate from B objects of A with no native representation in B</li>
-</ul>
-</li>
-</ul>
-</li>
-<li>
-<p><strong>Binding</strong></p>
-<ul>
-<li>
-<p>Originally: a pexpect interface</p>
-</li>
-<li>
-<p>Now: ABI (direct calls at the C level)</p>
-</li>
-</ul>
-</li>
-</ul><hr><ul>
-<li>
-<p><strong>Adapting</strong></p>
-<ul>
-<li>
-<p>Currently:</p>
-<ul>
-<li>monolithic adapters for some cases (groups, …)</li>
-</ul>
-</li>
-<li>
-<p>In progress:</p>
-<ul>
-<li>
-<p>modular adapters, exploiting the category hierarchy and semantic alignments</p>
-</li>
-<li>
-<p>objects returned as reference + semantic</p>
-</li>
-<li>
-<p>alignment <code>B.cardinality() -&gt; Size(A)</code> attached to the category of sets</p>
-</li>
-<li>
-<p>alignment <code>B.conjugacy_classes() -&gt; ConjugacyClasses(A)</code> attached to the category of groups</p>
-</li>
-</ul>
-</li>
-</ul>
-</li>
-</ul><hr><h2 id="Open-discussion" style=""><a class="anchor hidden-xs" href="#Open-discussion" title="Open-discussion"><span class="octicon octicon-link"></span></a>Open discussion</h2><ul>
-<li>
-<p>How to foster a sustainable and agile ecosystem where (sub)components have their own life cycle, explore new approaches, compete, and happily die when no more relevant.</p>
-</li>
-<li>
-<p>What other barriers do you identify in Computational Math?</p>
-</li>
-<li>
-<p>How do the barriers differ from other areas</p>
-</li>
-<li>
-<p>Other case studies? solutions? approaches?</p>
-</li>
-</ul></div>
-    <div class="ui-toc dropup unselectable hidden-print" style="display:none;">
-        <div class="pull-right dropdown">
-            <a id="tocLabel" class="ui-toc-label btn btn-default" data-toggle="dropdown" href="#" role="button" aria-haspopup="true" aria-expanded="false" title="Table of content">
-                <i class="fa fa-bars"></i>
-            </a>
-            <ul id="ui-toc" class="ui-toc-dropdown dropdown-menu" aria-labelledby="tocLabel">
-                <div class="toc"><ul class="nav"><li class=""><a href="#Modularity-in-Mathematical-Computation" title="Modularity in Mathematical Computation">Modularity in Mathematical Computation</a><ul class="nav"><li><a href="#A-collaborative-document" title="A collaborative document">A collaborative document</a></li><li><a href="#Participants" title="Participants">Participants</a></li><li><a href="#Abstract" title="Abstract">Abstract</a></li><li><a href="#Composability" title="Composability?">Composability?</a><ul class="nav"><li><a href="#Data-transfers" title="Data transfers">Data transfers</a></li><li><a href="#Procedure-calls" title="Procedure calls">Procedure calls</a></li></ul></li><li><a href="#Barriers-faced-by-the-computational-pure-maths-community" title="Barriers faced by the computational pure maths community?">Barriers faced by the computational pure maths community?</a><ul class="nav"><li><a href="#Semantic-barriers" title="Semantic barriers">Semantic barriers</a></li><li><a href="#Social-barriers" title="Social barriers">Social barriers</a></li><li><a href="#Technical-barriers" title="Technical barriers">Technical barriers</a></li></ul></li><li><a href="#Some-case-studies-and-tentative-solutions" title="Some case studies and tentative solutions">Some case studies and tentative solutions</a><ul class="nav"><li><a href="#OpenMath" title="OpenMath">OpenMath</a></li><li><a href="#The-Math-in-the-Middle-approach" title="The Math-in-the-Middle approach">The Math-in-the-Middle approach</a></li><li><a href="#Categories-in-GAP-Axiom-MuPAD-SageMath" title="Categories in GAP, Axiom, MuPAD, SageMath">Categories in GAP, Axiom, MuPAD, SageMath</a></li><li><a href="#Case-Study-libsemigroups-a-library-for-computing-with-semigroups" title="Case Study: libsemigroups:, a library for computing with semigroups">Case Study: libsemigroups:, a library for computing with semigroups</a></li><li><a href="#Case-Study-the-Sage--GAP-interface" title="Case Study: the Sage / GAP interface">Case Study: the Sage / GAP interface</a></li></ul></li><li><a href="#Open-discussion" title="Open discussion">Open discussion</a></li></ul></li></ul></div><div class="toc-menu"><a class="expand-toggle" href="#">Expand all</a><a class="back-to-top" href="#">Back to top</a><a class="go-to-bottom" href="#">Go to bottom</a></div>
-            </ul>
-        </div>
-    </div>
-    <div id="ui-toc-affix" class="ui-affix-toc ui-toc-dropdown unselectable hidden-print" data-spy="affix" style="top:17px;display:none;"  >
-        <div class="toc"><ul class="nav"><li class=""><a href="#Modularity-in-Mathematical-Computation" title="Modularity in Mathematical Computation">Modularity in Mathematical Computation</a><ul class="nav"><li><a href="#A-collaborative-document" title="A collaborative document">A collaborative document</a></li><li><a href="#Participants" title="Participants">Participants</a></li><li><a href="#Abstract" title="Abstract">Abstract</a></li><li><a href="#Composability" title="Composability?">Composability?</a><ul class="nav"><li><a href="#Data-transfers" title="Data transfers">Data transfers</a></li><li><a href="#Procedure-calls" title="Procedure calls">Procedure calls</a></li></ul></li><li><a href="#Barriers-faced-by-the-computational-pure-maths-community" title="Barriers faced by the computational pure maths community?">Barriers faced by the computational pure maths community?</a><ul class="nav"><li><a href="#Semantic-barriers" title="Semantic barriers">Semantic barriers</a></li><li><a href="#Social-barriers" title="Social barriers">Social barriers</a></li><li><a href="#Technical-barriers" title="Technical barriers">Technical barriers</a></li></ul></li><li><a href="#Some-case-studies-and-tentative-solutions" title="Some case studies and tentative solutions">Some case studies and tentative solutions</a><ul class="nav"><li><a href="#OpenMath" title="OpenMath">OpenMath</a></li><li><a href="#The-Math-in-the-Middle-approach" title="The Math-in-the-Middle approach">The Math-in-the-Middle approach</a></li><li><a href="#Categories-in-GAP-Axiom-MuPAD-SageMath" title="Categories in GAP, Axiom, MuPAD, SageMath">Categories in GAP, Axiom, MuPAD, SageMath</a></li><li><a href="#Case-Study-libsemigroups-a-library-for-computing-with-semigroups" title="Case Study: libsemigroups:, a library for computing with semigroups">Case Study: libsemigroups:, a library for computing with semigroups</a></li><li><a href="#Case-Study-the-Sage--GAP-interface" title="Case Study: the Sage / GAP interface">Case Study: the Sage / GAP interface</a></li></ul></li><li><a href="#Open-discussion" title="Open discussion">Open discussion</a></li></ul></li></ul></div><div class="toc-menu"><a class="expand-toggle" href="#">Expand all</a><a class="back-to-top" href="#">Back to top</a><a class="go-to-bottom" href="#">Go to bottom</a></div>
-    </div>
-    <script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.1.1/jquery.min.js" integrity="sha256-hVVnYaiADRTO2PzUGmuLJr8BLUSjGIZsDYGmIJLv2b8=" crossorigin="anonymous"></script>
-    <script src="https://cdnjs.cloudflare.com/ajax/libs/twitter-bootstrap/3.3.7/js/bootstrap.min.js" integrity="sha256-U5ZEeKfGNOja007MMD3YBI0A3OSZOQbeG6z2f2Y0hu8=" crossorigin="anonymous" defer></script>
-    <script src="https://cdnjs.cloudflare.com/ajax/libs/gist-embed/2.6.0/gist-embed.min.js" integrity="sha256-KyF2D6xPIJUW5sUDSs93vWyZm+1RzIpKCexxElmxl8g=" crossorigin="anonymous" defer></script>
-    <script>
-        var markdown = $(".markdown-body");
-        //smooth all hash trigger scrolling
-        function smoothHashScroll() {
-            var hashElements = $("a[href^='#']").toArray();
-            for (var i = 0; i < hashElements.length; i++) {
-                var element = hashElements[i];
-                var $element = $(element);
-                var hash = element.hash;
-                if (hash) {
-                    $element.on('click', function (e) {
-                        // store hash
-                        var hash = this.hash;
-                        if ($(hash).length <= 0) return;
-                        // prevent default anchor click behavior
-                        e.preventDefault();
-                        // animate
-                        $('body, html').stop(true, true).animate({
-                            scrollTop: $(hash).offset().top
-                        }, 100, "linear", function () {
-                            // when done, add hash to url
-                            // (default click behaviour)
-                            window.location.hash = hash;
-                        });
-                    });
-                }
-            }
-        }
-
-        smoothHashScroll();
-        var toc = $('.ui-toc');
-        var tocAffix = $('.ui-affix-toc');
-        var tocDropdown = $('.ui-toc-dropdown');
-        //toc
-        tocDropdown.click(function (e) {
-            e.stopPropagation();
-        });
-
-        var enoughForAffixToc = true;
-
-        function generateScrollspy() {
-            $(document.body).scrollspy({
-                target: ''
-            });
-            $(document.body).scrollspy('refresh');
-            if (enoughForAffixToc) {
-                toc.hide();
-                tocAffix.show();
-            } else {
-                tocAffix.hide();
-                toc.show();
-            }
-            $(document.body).scroll();
-        }
-
-        function windowResize() {
-            //toc right
-            var paddingRight = parseFloat(markdown.css('padding-right'));
-            var right = ($(window).width() - (markdown.offset().left + markdown.outerWidth() - paddingRight));
-            toc.css('right', right + 'px');
-            //affix toc left
-            var newbool;
-            var rightMargin = (markdown.parent().outerWidth() - markdown.outerWidth()) / 2;
-            //for ipad or wider device
-            if (rightMargin >= 133) {
-                newbool = true;
-                var affixLeftMargin = (tocAffix.outerWidth() - tocAffix.width()) / 2;
-                var left = markdown.offset().left + markdown.outerWidth() - affixLeftMargin;
-                tocAffix.css('left', left + 'px');
-            } else {
-                newbool = false;
-            }
-            if (newbool != enoughForAffixToc) {
-                enoughForAffixToc = newbool;
-                generateScrollspy();
-            }
-        }
-        $(window).resize(function () {
-            windowResize();
-        });
-        $(document).ready(function () {
-            windowResize();
-            generateScrollspy();
-        });
-
-        //remove hash
-        function removeHash() {
-            window.location.hash = '';
-        }
-
-        var backtotop = $('.back-to-top');
-        var gotobottom = $('.go-to-bottom');
-
-        backtotop.click(function (e) {
-            e.preventDefault();
-            e.stopPropagation();
-            if (scrollToTop)
-                scrollToTop();
-            removeHash();
-        });
-        gotobottom.click(function (e) {
-            e.preventDefault();
-            e.stopPropagation();
-            if (scrollToBottom)
-                scrollToBottom();
-            removeHash();
-        });
-
-        var toggle = $('.expand-toggle');
-        var tocExpand = false;
-
-        checkExpandToggle();
-        toggle.click(function (e) {
-            e.preventDefault();
-            e.stopPropagation();
-            tocExpand = !tocExpand;
-            checkExpandToggle();
-        })
-
-        function checkExpandToggle () {
-            var toc = $('.ui-toc-dropdown .toc');
-            var toggle = $('.expand-toggle');
-            if (!tocExpand) {
-                toc.removeClass('expand');
-                toggle.text('Expand all');
-            } else {
-                toc.addClass('expand');
-                toggle.text('Collapse all');
-            }
-        }
-
-        function scrollToTop() {
-            $('body, html').stop(true, true).animate({
-                scrollTop: 0
-            }, 100, "linear");
-        }
-
-        function scrollToBottom() {
-            $('body, html').stop(true, true).animate({
-                scrollTop: $(document.body)[0].scrollHeight
-            }, 100, "linear");
-        }
-    </script>
-</body>
-
-</html>
--- a/events/index.md
+++ b/events/index.md
@@ -2,6 +2,7 @@
 layout: page
 title: KWARC - Events 
 ---
-The Academic Events we organize
+Some smaller academic events we have organized that do not have separate homepages:

-* [Tetrapod Workshop at FLOC-2018](/events/Tetrapod-2018)
+* [Tetrapod Workshop at FLOC-2018](Tetrapod2018/index.html)
+* [GI Jahrestreffen Fachgruppe Deduktionssystem und Logic in der Informatik](GILogicWorkshops/index.html)
--- a/index.md
+++ b/index.md
@@ -5,11 +5,34 @@ title: Home

 The ability to *represent knowledge about the world* and to *draw logical inferences* is one of the central components of intelligent behavior, as a consequence, reasoning components of some form are at the heart of many artificial intelligence systems.

+#### Research
+
 The KWARC research group conducts research in knowledge representation and reasoning techniques with a view towards applications in knowledge management. 
 We extend techniques from [formal methods](http://kwarc.info/semantics.html#fm) so that they can be used in settings where formalization is either infeasible or too costly. 
 We concentrate on developing techniques for marking up the [structural semantics](http://kwarc.info/semantics.html#ssem) in technical documents. 
 This level of markup allows for offering interesting [knowledge management services](http://kwarc.info/projects/) without forcing the author to formalize the document contents.

+##### Approach: Corpus-based Meta-Mathematics
+In this title we have three components that warrant explanation: 
+1. **Mathematics**: we use the  mathematical knowledge and mathematical documents as a test
+  tube for our research as the knowledge and document structures are quite explicit and
+  overt and the content of mathematics is well-understood. Anything that has the same
+  properties we consider to be "mathematics" as well. 
+2. **Meta**: we develop Meta-Artefacts, i.e. we
+   * design **representation languages** (logics) that allow to talk *about* mathematical objects,
+   their properties, and relations,
+   * invent **algorithms** that analyze and transform these representations, and
+   * implement them in **end-user systems** that utilize both. 
+3. **Corpus-based**: we do this as a natural science by looking at data (i.e. corpora of
+documents and formalizations).
+
+##### KWARC Process
+We approach Corpus-Based Meta-Mathematics (iteratively) in three steps:
+1. **Analysis**: we analyze the corpora for patterns and structures.
+2. **Synthesis**: we design and build meta-artefacts (languages, algorithms, and systems)
+and derive data sets from the corpora.
+3. **Experimentation**: we evaluate the representation languages and algorithms on the
+   corpora and the systems on end users (mathematicians).

 #### Recent News ([see all](/news/))
 
@@ -18,3 +41,6 @@ This level of markup allows for offering interesting [knowledge management servi
        {% include post_link.html post=post %}
    {% endfor %}
 </ul>
+
+<!--  LocalWords:  endfor analyze
+ -->
--- a/people/achugh.md
+++ b/people/achugh.md
+---
+layout: person
+
+title: Abhishek Chugh
+fullname: M.Sc. Abhishek Chugh
+pic: public/images/abchugh.png
+
+role: Research Engineer
+start_date: 2022-05
+
+publink: https://linkedin.com/in/abhishekchugh
+
+website: https://sophize.org
+affiliation: Sophize Foundation
+---
+
+### Description
+
+I am a software engineer and has worked on products such as Adobe Illustrator, Google Maps and Google Pay. I am passionate about organizing knowledge from different perspectives in a way that allows readers to effortlessly see all kinds of justifications for and against any claim. To further this goal, I started Sophize Foundation, a non-profit that is currently working towards building an open state-of-the-art [Mathematics library](https://sophize.org).
+
+### Research Focus
+
+As a KWARCie, I am very excited to help build systems and interfaces that will generate and present educational material tailored to each learner's specific needs.
--- a/people/ahambasan.md
+++ b/people/ahambasan.md
@@ -7,6 +7,7 @@ fullname: Alexandru Hambasan
 role: bachelor-student
 pic: public/images/ahambasan.jpeg
 start_date: 2017-03
+end_date: 2018-01

 affiliation: Jacobs Unviersity Bremen
 ---

--- a/people/akohlhase.md
+++ b/people/akohlhase.md
@@ -9,7 +9,13 @@ role: postdoc
 start_date: 2005-12
 end_date: 2014-08

+dblp: k/Kohlhase:Andrea
+researchgate: Andrea_Kohlhase2
+github: akohlhase
+mathhub: akohlhase
+zbmath: kohlhase.andrea
 publink: auto
+orcid: 0000-0001-5384-6702

 affiliation: Hochschule Neu-Ulm
 website: https://www.hs-neu-ulm.de/andrea-kohlhase/

--- a/people/aschmidt.md
+++ b/people/aschmidt.md
+---
+layout: person
+
+title: Annika Schmidt
+fullname: B.Sc. Annika Schmidt
+pic: public/images/aschmidt.png
+
+start_date: 2020-10
+end_date: 2021-11
+role: master-student
+affiliation: Computer Science, FAU Erlangen-Nürnberg
+
+NOpublink: auto
+
+NOwebsite:
+---
+### Description  
+
+I am a master student at [FAU Erlangen-Nürnberg](http://www.fau.de). Currently I am working on my master thesis at the [KWARC group](http://kwarc.info) and got employed there as a Hiwi to help with the AI-1 lecture.
+
+In 2015 I started studying Computer Science at [FAU Erlangen-Nürnberg](http://www.fau.de). While finishing my bachelor's degree I visited some master courses. My main interests are optimization and artificial intelligence. Also, I am very interested in knowledge management and gaining new knowledge.
+
+### Current Work
+
+My master thesis is about the formalization of set theory in [KWARC's MMT system](https://kwarc.info/systems/mmt/). To achieve this goal I use some old formalizations of set theory in Twelf. Since I just started the exact course of my master thesis is still unclarified.
+
+My work as a Hiwi mostly consists of cutting old lecture videos to make online lectures more attractive for students. Also, I give advice and help to come up with good questions for the students.
+
+### Contact
+
+Feel free to contact me at annika.as.schmidt@fau.de.
No results found