IMPS
From MaRDI portal
Software:21136
swMATH9143MaRDI QIDQ21136FDOQ21136
Author name not available (Why is that?)
Cited In (50)
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- Title not available (Why is that?)
- A formalization of metric spaces in HOL Light
- A realizability interpretation of Church's simple theory of types
- Lax Theory Morphisms
- A scalable module system
- Towards Knowledge Management for HOL Light
- Adapting functional programs to higher order logic
- Computer algebra and artificial intelligence
- The seven virtues of simple type theory
- Automating Change of Representation for Proofs in Discrete Mathematics
- Title not available (Why is that?)
- Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates
- Mechanizing set theory. Cardinal arithmetic and the axiom of choice
- Analytica --- an experiment in combining theorem proving and symbolic computation
- A formal framework for managing mathematics
- Incorporating quotation and evaluation into Church's type theory
- MBase: Representing knowledge and context for the integration of mathematical software systems
- State and progress in strand spaces: proving fair exchange
- Residual theory in λ-calculus: a formal development
- Walther recursion
- Instantiation theory. On the foundations of automated deduction
- Automating change of representation for proofs in discrete mathematics (extended version)
- An approach to literate and structured formal developments
- QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
- Organizing numerical theories using axiomatic type classes
- Proof script pragmatics in IMPS
- A module system for a programming language based on the LF logical framework
- Crystal: Integrating structured queries into a tactic language
- Title not available (Why is that?)
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- Panoptes
- Title not available (Why is that?)
- Verification: Theory and Practice
- TPS: A theorem-proving system for classical type theory
- Automatically finding theory morphisms for knowledge management
- Translating the IMPS theory library to MMT/OMDoc
- Mathematical Knowledge Management
- A fixedpoint approach to implementing (Co)inductive definitions
- A two-valued logic for properties of strict functional programs allowing partial functions
- TPS: A hybrid automatic-interactive system for developing proofs
- The Watson theorem prover
- An overview of a formal framework for managing mathematics
- Experiences from exporting major proof assistant libraries
- A mechanization of strong Kleene logic for partial functions
- Deduction as an Engineering Science
- IMPS: An updated system description
- A partial functions version of Church's simple theory of types
- A simple type theory with partial functions and subtypes
- Formalizing mathematical knowledge as a biform theory graph: a case study
This page was built for software: IMPS
