scientific article; zbMATH DE number 7756106
From MaRDI portal
Publication:6079227
DOI10.4230/lipics.types.2019.1arXiv2005.08884MaRDI QIDQ6079227
Makarius Wenzel, Florian Rabe, Michael Kohlhase
Publication date: 27 October 2023
Full work available at URL: https://arxiv.org/abs/2005.08884
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- A scalable module system
- Making PVS accessible to generic services by interpretation in a universal format
- Translating the IMPS theory library to MMT/OMDoc
- Automatically finding theory morphisms for knowledge management
- Edinburgh LCF. A mechanized logic of computation
- The Mizar Mathematical Library in OMDoc: translation and applications
- HOL(y)Hammer: online ATP service for HOL Light
- Towards a heterogeneous query language for mathematical knowledge
- Representing structural language features in formal meta-languages
- From LCF to Isabelle/HOL
- Interaction with formal mathematical documents in Isabelle/PIDE
- Relational data across mathematical libraries
- The Coq library as a theory graph
- Locales: a module system for mathematical theories
- Translating higher-order clauses to first-order clauses
- Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
- Challenges and Experiences in Managing Large-Scale Proofs
- Extending MKM Formats at the Statement Level
- How to identify, translate and combine logics?
- Constructive Type Classes in Isabelle
- Local Theory Specifications in Isabelle/Isar
- A framework for defining logics
- QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
- A Search Engine for Mathematical Formulae
- Scalable LCF-Style Proof Translation
- Matching Concepts across HOL Libraries
- Towards Knowledge Management for HOL Light
- Importing HOL Light into Coq
- A Mechanized Translation from Higher-Order Logic to Set Theory
This page was built for publication:
