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