Kai Amann	University Erlangen-Nuremberg, Erlangen, Germany	Integrating Semantic Mathematical Documents and Dynamic Notebooks
A. Asperti		Intelligent Computer Mathematics, Work-in-Progress Proceedings
D. Aspinall		Workshops and Work in Progress at CICM 2013
Steve Awodey	Carnegie Mellon University, Pittsburgh, USA	Kripke Semantics for Martin-Löf's Extensional Type Theory Kripke Semantics for Martin-Löf's Extensional Type Theory
A. Bauer		Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401)
Christoph Benzmüller	Freie Universität, Berlin, Germany	THF0 -- The core of the TPTP Language for Higher-Order Logic
C. Benzmüller		Theorem Proving in Dependently Typed Higher-Order Logic
M. Berges		The Potential of Answer Classes in Large-scale Written Computer Science Exams
Katja Berčič	University Erlangen-Nuremberg, Erlangen, Germany	Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401) (Deep) FAIR Mathematics Towards a Heterogeneous Query Language for Mathematical Knowledge Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation
R. Bird		How to calculate with nondeterministic functions
J. Carette		Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge Intelligent Computer Mathematics Workshops and Work in Progress at CICM 2013
Mihai Codescu	DFKI, Bremen, Germany	Canonical Selection of Colimits Compiling Logics A Proof Theoretic Interpretation of Model Theoretic Hiding Towards Logical Frameworks in the Heterogeneous Tool Set Hets Project Abstract: Logic Atlas and Integrator (LATIN)
A. Condoluci		Relational Data Across Mathematical Libraries
J. Davenport		Workshops and Work in Progress at CICM 2013 Intelligent Computer Mathematics Intelligent Computer Mathematics, Work-in-Progress Proceedings
Catalin David	Jacobs University, Bremen, Germany	Publishing Math Lecture Notes as Linked Data
P. Dehaye		Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach
M. England		Intelligent Computer Mathematics
W. Farmer		Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge Intelligent Computer Mathematics Intelligent Computer Mathematics Intelligent Computer Mathematics, Work-in-Progress Proceedings
T. Gauthier		Classification of Alignments between Concepts of Formal Mathematical Systems
H. Geuvers		Intelligent Computer Mathematics LFMTP 2011 - MLPA 2011 Informal Proceedings
Jana Gičeva	ETH Zürich, Zürich, Switzerland	Integrating Web Services into Active Mathematical Documents
Joseph Goguen	University of California at San Diego, San Diego, USA	An Institutional View on Categorical Logic
O. Hasan		Workshop Papers at CICM 2018 Intelligent Computer Mathematics
Fulya Horozal	Jacobs University, Bremen, Germany	Formal Logic Definitions for Interchange Languages Flexary Operators for Formalized Mathematics Compiling Logics A Proof Theoretic Interpretation of Model Theoretic Hiding Extending MKM Formats at the Statement Level Towards Logical Frameworks in the Heterogeneous Tool Set Hets Representing Model Theory in a Type-Theoretical Logical Framework Combining Source, Content, Presentation, Narration, and Relational Representation Project Abstract: Logic Atlas and Integrator (LATIN) Representing Model Theory in a Type-Theoretical Logical Framework
Alin Iacob	Jacobs University, Bremen, Germany	Combining Source, Content, Presentation, Narration, and Relational Representation
Mihnea Iancu	Jacobs University, Bremen, Germany	Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach The Mizar Mathematical Library in OMDoc: Translation and Applications Management of Change in Declarative Languages (Work-in-Progress) An MMT-Based User-Interface Formalizing Foundations of Mathematics
Aivaras Jakubauskas	Jacobs University, Bremen, Germany	Compiling Logics
G. Jaloyan		Enhancing Proof Stability
Constantin Jucovschi	Jacobs University, Bremen, Germany	Combining Source, Content, Presentation, Narration, and Relational Representation
Cezary Kaliszyk	University of Innsbruck, Innsbruck, Austria	A Survey of Languages for Formalizing Mathematics Classification of Alignments between Concepts of Formal Mathematical Systems TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism
C. Kaliszyk		Intelligent Computer Mathematics Towards Knowledge Management for HOL Light
M. Kerber		Intelligent Computer Mathematics
Michael Kohlhase	Jacobs University, Bremen, Germany	The Potential of Answer Classes in Large-scale Written Computer Science Exams Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge Experiences from Exporting Major Proof Assistant Libraries (Deep) FAIR Mathematics 3-Dimensional Graph Visualization of Mathematical Knowledge Logic-Independent Proof Search in Logical Frameworks (short paper) Representing Structural Language Features in Formal Meta-Languages Towards a Heterogeneous Query Language for Mathematical Knowledge Integrating Semantic Mathematical Documents and Dynamic Notebooks Making Isabelle Content Accessible in Knowledge Representation Formats Relational Data Across Mathematical Libraries Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation Model pathway diagrams for the representation of mathematical models Automatically Finding Theory Morphisms for Knowledge Management Theories as Types Classification of Alignments between Concepts of Formal Mathematical Systems Knowledge-Based Interoperability for Mathematical Software Systems Making PVS Accessible to Generic Services by Interpretation in a Universal Format Virtual Theories -- A Uniform Interface to Mathematical Knowledge Bases QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach Flexary Operators for Formalized Mathematics A Scalable Module System The Mizar Mathematical Library in OMDoc: Translation and Applications A Universal Machine for Biform Theory Graphs Semantics of OpenMath and MathML3 A Proof Theoretic Interpretation of Model Theoretic Hiding Extending MKM Formats at the Statement Level Towards Logical Frameworks in the Heterogeneous Tool Set Hets A Foundational View on Integration Problems Combining Source, Content, Presentation, Narration, and Relational Representation Project Abstract: Logic Atlas and Integrator (LATIN) A [insert XML Format] Database for [insert cool application] Publishing Math Lecture Notes as Linked Data Towards MKM in the Large: Modular Representation and Scalable Software Architecture Notations for Living Mathematical Documents An Exchange Format for Modular Knowledge
A. Kohlhase		Workshops and Work in Progress at CICM 2013
M. Kohlhase		Workshops and Work in Progress at CICM 2013
A. Konovalov		Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach
T. Koprucki		Model pathway diagrams for the representation of mathematical models
A. Kornilowicz		A New Export of the Mizar Mathematical Library
C. Lange		Workshops and Work in Progress at CICM 2013
Christoph Lange	Jacobs University, Bremen, Germany	Publishing Math Lecture Notes as Linked Data Integrating Web Services into Active Mathematical Documents Flyspeck in a Semantic Wiki
S. Lelièvre		Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach
P. Libbrecht		Workshops and Work in Progress at CICM 2013
Yufei Liu	Jacobs University, Bremen, Germany	Alignment-based Translations Across Formal Systems Using Interface Theories
D. Lohr		The Potential of Answer Classes in Large-scale Written Computer Science Exams
Felix Mance	ETH Zürich, Zürich, Switzerland	A Universal Machine for Biform Theory Graphs
Richard Marcus	University Erlangen-Nuremberg, Erlangen, Germany	3-Dimensional Graph Visualization of Mathematical Knowledge
Sean McLaughlin	Carnegie Mellon University, Pittsburgh, USA	Flyspeck in a Semantic Wiki
S. McLaughlin		Retaining Dafny Specifications Enhancing Proof Stability
M. Miculan		LFMTP: Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice LFMTP: Work-in-Progress Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice
Till Mossakowski	DFKI, Bremen, Germany	Canonical Selection of Colimits Compiling Logics A Proof Theoretic Interpretation of Model Theoretic Hiding Towards Logical Frameworks in the Heterogeneous Tool Set Hets Project Abstract: Logic Atlas and Integrator (LATIN) An Institutional View on Categorical Logic
Dennis Müller	University Erlangen-Nuremberg, Erlangen, Germany	Representing Structural Language Features in Formal Meta-Languages Relational Data Across Mathematical Libraries Structuring Theories with Implicit Morphisms The Coq Library as a Theory Graph Rapid Prototyping Formal Systems in MMT: Case Studies Model pathway diagrams for the representation of mathematical models Automatically Finding Theory Morphisms for Knowledge Management Theories as Types Classification of Alignments between Concepts of Formal Mathematical Systems Knowledge-Based Interoperability for Mathematical Software Systems Making PVS Accessible to Generic Services by Interpretation in a Universal Format Alignment-based Translations Across Formal Systems Using Interface Theories Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach
Christine Müller	Jacobs University, Bremen, Germany	Notations for Living Mathematical Documents
G. Nadathur		LFMTP 2011 - MLPA 2011 Informal Proceedings
S. Owre		Making PVS Accessible to Generic Services by Interpretation in a Universal Format
G. Passmore		Intelligent Computer Mathematics
M. Pfeiffer		Knowledge-Based Interoperability for Mathematical Software Systems Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach
P. Pudlák		Solving the $100 Modal Logic Challenge
P. Quaresma		Workshops and Work in Progress at CICM 2013
M. Rapoport		Retaining Dafny Specifications
Colin Rothgang	Jacobs University, Bremen, Germany	Theorem Proving in Dependently Typed Higher-Order Logic A New Export of the Mizar Mathematical Library Representing Structural Language Features in Formal Meta-Languages Alignment-based Translations Across Formal Systems Using Interface Theories
Navid Roux	University Erlangen-Nuremberg, Erlangen, Germany	Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style Structure-Preserving Diagram Operators
N. Runga		Retaining Dafny Specifications
Claudio Sacerdoti Coen	University of Bologna, Bologna, Italy	Logic-Independent Proof Search in Logical Frameworks (short paper) Relational Data Across Mathematical Libraries The Coq Library as a Theory Graph A Foundational View on Integration Problems
Jan Frederik Schaefer	University Erlangen-Nuremberg, Erlangen, Germany	Logic-Independent Proof Search in Logical Frameworks (short paper)
Steffen Schlager	University of Karlsruhe, Karlsruhe, Germany	A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela$^+$
M. Schlaipfer		Retaining Dafny Specifications
Peter Schmitt	University of Karlsruhe, Karlsruhe, Germany	A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela$^+$
Lutz Schröder	DFKI, Bremen, Germany	An Institutional View on Categorical Logic
Carsten Schürmann	IT University, Copenhagen, Denmark	LFMTP 2011 - MLPA 2011 Informal Proceedings MLPA '10: Proceedings of the 2nd Workshop on Modules and Libraries for Proof Assistants MLPA '09: Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants A Practical Module System for LF
Y. Sharoda		Diagram Operators in MMT
W. Shen		Solving the $100 Modal Logic Challenge
Kristina Sojakova	Carnegie Mellon University, Pittsburgh, USA	Logical Relations for a Logical Framework Towards Logical Frameworks in the Heterogeneous Tool Set Hets Translating a Dependently-Typed Logic to First-Order Logic
P. Sojka		Workshops and Work in Progress at CICM 2013
V. Sorge		Intelligent Computer Mathematics
Geoff Sutcliffe	University of Miami, Miami, USA	TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism THF0 -- The core of the TPTP Language for Higher-Order Logic Solving the $100 Modal Logic Challenge
K. Tabelow		Model pathway diagrams for the representation of mathematical models
J. Taslak		Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401)
O. Teschke		Intelligent Computer Mathematics
N. Thiéry		Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401) Knowledge-Based Interoperability for Mathematical Software Systems Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach
Josef Urban	Radboud University, Nijmegen, The Netherlands	The Mizar Mathematical Library in OMDoc: Translation and Applications Intelligent Computer Mathematics Intelligent Computer Mathematics, Work-in-Progress Proceedings
V. Vasilyev		Knowledge-Based Interoperability for Mathematical Software Systems
S. Watt		Extracting Theory Graphs from Aldor Libraries
Franzika Weber	University Erlangen-Nuremberg, Erlangen, Germany	Morphism Equality in Theory Graphs
M. Wenzel		Making Isabelle Content Accessible in Knowledge Representation Formats Relational Data Across Mathematical Libraries
I. Whiteside		Workshops and Work in Progress at CICM 2013
Tom Wiesing	University Erlangen-Nuremberg, Erlangen, Germany	Integrating Semantic Mathematical Documents and Dynamic Notebooks Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach
T. Wiesing		Knowledge-Based Interoperability for Mathematical Software Systems Virtual Theories -- A Uniform Interface to Mathematical Knowledge Bases
W. Windsteiger		Workshops and Work in Progress at CICM 2013
T. Xiang		Retaining Dafny Specifications Enhancing Proof Stability
A. Youssef		Intelligent Computer Mathematics
Vyacheslav Zholudev	Jacobs University, Bremen, Germany	A [insert XML Format] Database for [insert cool application] Publishing Math Lecture Notes as Linked Data Towards MKM in the Large: Modular Representation and Scalable Software Architecture
Valeria de Paiva	Palo Alto Research Center, Palo Alto, USA	An Institutional View on Categorical Logic
19 others		Workshop Papers at CICM 2018