Pages that link to "Item:Q1319391"

The following pages link to IMPS: An interactive mathematical proof system (Q1319391):

Displaying 37 items.

• IMPS (Q21136) (← links)
• 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)
• 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)
• An approach to literate and structured formal developments (Q1911317) (← links)
• TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
• Experiences from exporting major proof assistant libraries (Q2069875) (← links)
• Joshua Guttman: pioneering strand spaces (Q2154021) (← links)
• Structuring theories with implicit morphisms (Q2185893) (← links)
• Structure-preserving diagram operators (Q2237343) (← 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)
• Formalising foundations of mathematics (Q3094180) (← links)
• Automating Change of Representation for Proofs in Discrete Mathematics (Q3453117) (← links)
• A realizability interpretation of Church's simple theory of types (Q4593235) (← links)
• IMPS: An updated system description (Q4647527) (← links)
• Walther recursion (Q4647554) (← links)
• Deduction as an Engineering Science (Q4916217) (← links)
• Panoptes (Q5166496) (← links)
• A fixedpoint approach to implementing (Co)inductive definitions (Q5210768) (← links)
• Proof script pragmatics in IMPS (Q5210784) (← links)
• A mechanization of strong Kleene logic for partial functions (Q5210785) (← links)
• Lax Theory Morphisms (Q5277906) (← links)
• Towards Knowledge Management for HOL Light (Q5495935) (← links)
• MBase: Representing knowledge and context for the integration of mathematical software systems (Q5950933) (← links)
• Elements of mathematical analysis in PVS (Q6567709) (← links)
• Set theory, higher order logic or both? (Q6567712) (← links)