The following pages link to IMPS (Q21136):
Displaying 29 items.
- A two-valued logic for properties of strict functional programs allowing partial functions (Q352946) (← links)
- A scalable module system (Q391632) (← links)
- State and progress in strand spaces: proving fair exchange (Q437028) (← links)
- A formalization of metric spaces in HOL Light (Q682381) (← links)
- TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- Adapting functional programs to higher order logic (Q1029815) (← links)
- Instantiation theory. On the foundations of automated deduction (Q1202066) (← links)
- Analytica --- an experiment in combining theorem proving and symbolic computation (Q1272608) (← links)
- A simple type theory with partial functions and subtypes (Q1314643) (← links)
- Computer algebra and artificial intelligence (Q1404691) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- Organizing numerical theories using axiomatic type classes (Q1774558) (← links)
- Translating the IMPS theory library to MMT/OMDoc (Q1798938) (← links)
- Automatically finding theory morphisms for knowledge management (Q1798969) (← links)
- An overview of a formal framework for managing mathematics (Q1810918) (← links)
- An approach to literate and structured formal developments (Q1911317) (← links)
- TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L (Q1961914) (← links)
- Experiences from exporting major proof assistant libraries (Q2069875) (← links)
- Formalizing mathematical knowledge as a biform theory graph: a case study (Q2364688) (← links)
- Automating change of representation for proofs in discrete mathematics (extended version) (Q2364883) (← links)
- Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates (Q2457362) (← links)
- Crystal: Integrating structured queries into a tactic language (Q2655333) (← links)
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge (Q2663667) (← links)
- (Q2767940) (← links)
- (Q3086786) (← links)
- Panoptes (Q5166496) (← links)
- QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge (Q5195275) (← links)
