It is my pleasure to announce the second in the series of online seminars on proof assistants. MMT: A Foundation-Independent Logical System Time: Thursday, May 21, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2) Location: online at Zoom ID 989 0478 8985 (https://zoom.us/j/98904788985) Speaker: Florian Rabe (University of Erlangen) (https://kwarc.info/people/frabe/) Proof assistant: The MMT Language and System (https://uniformal.github.io/) Abstract: Logical frameworks are meta-logics for defining other logics. MMT follows this approach but abstracts even further: it avoids committing to any foundational features like function types or propositions. All MMT algorithms are parametric in a set of rules, which are self-contained objects plugged in by the language designer. That results in a framework general enough to develop many formal systems including other logical frameworks in it, enabling the rapid prototyping of new language features. Despite this high level of generality, it is possible to develop sophisticated results in MMT. The current release includes, e.g., parsing, type reconstruction, module system, IDE-style editor, and interactive library browser. MMT is systematically designed to be extensible, providing multiple APIs and plugin interfaces, and thus provides a versatile infrastructure for system development and integration. This talk gives an overview of the current state of MMT and its future challenges. Examples are drawn from the LATIN project, a long-running project of building a modular, highly inter-related suite of formalizations of logics and related formal systems. After the talk, the video recording will be made available. Also see the anouncement on my blog at http://math.andrej.com/2020/05/15/mmt-a-foundation-independent-logical-system/ The spring schedule of talks is planned as follows: May 28, 2020: Brigitte Pientka - Beluga June 11, 2020: Conor McBride - Epigram 2 June 25, 2020: William J. Bowman, Cur July 2, 2020: Anders Mörtberg - cubicaltt (to be confirmed) July 9, 2020: Jon Sterling - redtt (to be confirmed) With kind regards, Andrej -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB0nkh2Q_YFsZEZDq0qx9EudT3dO5yaSFPWP5hVWtJSgykkrnQ%40mail.gmail.com.