Cited in
(89)- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- A formalization of metric spaces in HOL Light
- scientific article; zbMATH DE number 1863385 (Why is no real title available?)
- A realizability interpretation of Church's simple theory of types
- A fixedpoint approach to implementing (co)inductive definitions
- A scalable module system
- Adapting functional programs to higher order logic
- Towards Knowledge Management for HOL Light
- Computer algebra and artificial intelligence
- The seven virtues of simple type theory
- Automating Change of Representation for Proofs in Discrete Mathematics
- Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates
- scientific article; zbMATH DE number 5872266 (Why is no real title available?)
- Deduction as an engineering science
- Analytica --- an experiment in combining theorem proving and symbolic computation
- Mechanizing set theory. Cardinal arithmetic and the axiom of choice
- A formal framework for managing mathematics
- Incorporating quotation and evaluation into Church's type theory
- State and progress in strand spaces: proving fair exchange
- MBase: Representing knowledge and context for the integration of mathematical software systems
- Residual theory in λ-calculus: a formal development
- Instantiation theory. On the foundations of automated deduction
- Walther recursion
- 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
- Proof script pragmatics in IMPS
- A module system for a programming language based on the LF logical framework
- Proviola
- OMRS
- MAYA
- MathWebSearch
- ETPS
- Nuprl
- Hets
- MMT
- OMDoc
- QMT
- STEXIDE
- MathXpert
- ALF
- Panoptes
- MetaOCaml
- Analytica
- PolyTOIL
- OpenDreamKit
- Lambda-Clam
- LATIN
- theoremprover-museum
- Elf
- reFLect
- VeriFun
- Mathpert
- GitLab
- Watson
- Emacs
- Gallina
- TGView
- Depth First Search
- HOL Light QE
- EVES
- Secondary Sylow
- PROVERB
- MathML
- Regexp
- Whelp
- Crystal: Integrating structured queries into a tactic language
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- scientific article; zbMATH DE number 1420790 (Why is no real title available?)
- scientific article; zbMATH DE number 1863381 (Why is no real title available?)
- 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
- Caml
- An overview of a formal framework for managing mathematics
- Experiences from exporting major proof assistant libraries
- The Watson theorem prover
- 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 simple type theory with partial functions and subtypes
- A partial functions version of Church's simple theory of types
- Notes from the logbook of a proof-checker's project
- Panoptes: an exploration tool for formal proofs
- Formalizing mathematical knowledge as a biform theory graph: a case study
This page was built for software: IMPS
