swMATH9143MaRDI QIDQ21136FDOQ21136
Author name not available (Why is that?)
Official website: http://imps.mcmaster.ca/
Cited In (73)
- Deduction as an engineering science
- Walther recursion
- Proof script pragmatics in IMPS
- 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 fixedpoint approach to implementing (co)inductive definitions
- A realizability interpretation of Church's simple theory of types
- 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
- Instantiation theory. On the foundations of automated deduction
- Lax theory morphisms
- Automating change of representation for proofs in discrete mathematics (extended version)
- An approach to literate and structured formal developments
- Organizing numerical theories using axiomatic type classes
- A module system for a programming language based on the LF logical framework
- Crystal: Integrating structured queries into a tactic language
- MAYA
- ETPS
- Nuprl
- Hets
- MMT
- QMT
- Title not available (Why is that?)
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- STEXIDE
- MathXpert
- ALF
- Panoptes
- MetaOCaml
- Analytica
- PolyTOIL
- OpenDreamKit
- Title not available (Why is that?)
- Lambda-Clam
- LATIN
- theoremprover-museum
- Elf
- VeriFun
- TGView
- HOL Light QE
- Secondary Sylow
- 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 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
- QED reloaded: towards a pluralistic formal library of mathematical knowledge
- IMPS: An updated system description
- A partial functions version of Church's simple theory of types
- Notes from the logbook of a proof-checker's project
- A simple type theory with partial functions and subtypes
- Panoptes: an exploration tool for formal proofs
- Caml
- Formalizing mathematical knowledge as a biform theory graph: a case study
This page was built for software: IMPS
