You must enable JavaScript to use this site

List of EventsInvited Talks [I1] Alan Bundy. Reformation: A Generic Algorithm for Repairing Faulty Logical Theories
 [I2] Przemyslaw Chojecki. DeepAlgebra  an outline of a program
 [I3] Grant Passmore. Formal Verification of Financial Algorithms, Progress and Prospects
Calculemus [C1] William Farmer and Jacques Carette. Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study
 [C2] Alexander Maletzky and Wolfgang Windsteiger. The Formalization ofVickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema
 [C3] Franck Slama and Edwin Brady. Automatically Proving Equivalence by TypeSafe Reflection
Digital Mathematical Libraries [D1] Patrick Ion and Stephen Watt. The Global Digital Mathematics Library and The International Mathematical Knowledge Trust
 [D2] Olivier Labbe and Thierry Bouche. The New Numdam platform
 [D3] Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase and Florian Rabe. Classification of Alignments between Concepts of Formal Mathematical Systems
 [D4] Wolfram Sperber and Michael Kohlhase. Software Citations, swMATH, and Beyond
Mathematical Knowledge Management [M1] Marco B. Caminati and Juliana Küster Filipe Bowles. A Verified Algorithm Enumerating Event Structures
 [M2] Howard Cohl, Moritz Schubotz, Abdou Youssef, André GreinerPetter, Jürgen Gerhard, Bonita V. Saunders, Marjorie A. McClain, Joon Bang and Kevin Chen. Semantic Preserving Bijective Mappings of Mathematical Formulae between Word Processors and Computer Algebra Systems
 [M3] Joseph Corneli, Ursula Martin, Dave MurrayRust and Alison Pease. Towards mathematical AI via a model of the content and process of mathematical question and answer dialogues
 [M4] William Farmer. Theory Morphisms in Church's Type Theory with Quotation and Evaluation
 [M5] Ian Ford. Semantic Representation of General Topology in the Wolfram Language
 [M6] Andreas Holmstrom and Torstein Vik. Zeta types and Tannakian symbols as a method for representing mathematical knowledge
 [M7] Cezary Kaliszyk and Karol Pąk. Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic
 [M8] Andrea Kohlhase, Michael Kohlhase and Michael Fürsich. Visual Structure in Math Expressions
 [M9] Michael Kohlhase, Thomas Koprucki, Dennis Müller and Karsten Tabelow. Mathematical Models as Research Data via Flexiformal Theory Graphs
 [M10] Zohreh Shams, Mateja Jamink, Gem Stapleton and Yuri Sato. Reasoning with Concept Diagrams about Antipatterns in Ontologies
Systems & Projects [S1] Nathan Carter and Kenneth Monks. A WebBased Toolkit for Mathematical Word Processing Applications with Semantics
 [S2] Jan Jakubuv and Josef Urban. ENIGMA: Efficient Learningbased Inference Guiding Machine
 [S3] Ekaterina Komendantskaya and Jónathan Heras. Proof mining with dependent types
 [S4] Adnan Rashid and Osman Hasan. Formalization of Transform Methods using HOL Light
 [S5] Usman Sanwal and Umair Siddique. Combining Refinement and SignalTemporal Logic for Biological Systems
 [S6] Moritz Schubotz, Norman Meuschke, Thomas Hepp, Howard Cohl and Bela Gipp. VMEXT: A Visualization Tool for Mathematical Expression Trees
 [S7] Abdou Youssef. PartofMath Tagging and Applications
Work in progress [W1] Catherine Dubois, Thérèse Hardin, François Pesseaux and Renaud Rioboo. Proving mathematical libraries: FoCaLiZe polynomials
 [W2] Carlos E. Freites. Mathdialog: a contextual ZFC syntactical game
 [W3] Alexander Maletzky. A New Reasoning Framework for Theorema 2.0
 [W4] Adam Naumowicz. Towards Standardized Mizar Environments
 [W5] Patrick Ion and Eric Weisstein. The Special Function Concordance
Business Meetings


Privacy policy and legal information
Last modified: February 15 2020 20:04:17 CET