The following pages link to Matita (Q18274):
Displaying 50 items.
- Reverse complexity (Q287279) (← links)
- Towards ``mouldable code'' via nested code graph transformation (Q406453) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- Tactics for hierarchical proof (Q626933) (← links)
- A formalization of multi-tape Turing machines (Q744986) (← links)
- Spurious disambiguation errors and how to get rid of them (Q841693) (← links)
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- From types to sets by local type definition in higher-order logic (Q1722645) (← links)
- Formal metatheory of programming languages in the Matita interactive theorem prover (Q1945919) (← links)
- Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean} (Q2097420) (← links)
- From the universality of mathematical truth to the interoperability of proof systems (Q2104491) (← links)
- The Coq library as a theory graph (Q2287907) (← links)
- A plugin to export Coq libraries to XML (Q2287917) (← links)
- Deciding Kleene algebra terms equivalence in Coq (Q2347910) (← links)
- Towards semantic mathematical editing (Q2348287) (← links)
- A canonical locally named representation of binding (Q2392482) (← links)
- Declarative representation of proof terms (Q2655330) (← links)
- Procedural representation of CIC proof terms (Q2655331) (← links)
- Crystal: Integrating structured queries into a tactic language (Q2655333) (← links)
- A study on fractional differential equations using the fractional Fourier transform (Q2668819) (← links)
- Congruence Closure in Intensional Type Theory (Q2817913) (← links)
- From Types to Sets by Local Type Definitions in Higher-Order Logic (Q2829259) (← links)
- Incompleteness, Undecidability and Automated Proofs (Q2829997) (← links)
- Tinycals: Step by Step Tacticals (Q2867943) (← links)
- Asynchronous User Interaction and Tool Integration in Isabelle/PIDE (Q2879273) (← links)
- A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions (Q2881085) (← links)
- A Web Interface for Matita (Q2907340) (← links)
- A Compact Proof of Decidability for Regular Expression Equivalence (Q2914749) (← links)
- A Language of Patterns for Subterm Selection (Q2914755) (← links)
- Formalizing Turing Machines (Q2915013) (← links)
- A Formal Proof of Borodin-Trakhtenbrot’s Gap Theorem (Q2938046) (← links)
- Computational Complexity Via Finite Types (Q2946764) (← links)
- Foundational extensible corecursion: a proof assistant perspective (Q2981955) (← links)
- Friends with Benefits (Q2988636) (← links)
- On Choice Rules in Dependent Type Theory (Q2988806) (← links)
- The swap of integral and limit in constructive mathematics (Q3053233) (← links)
- (Q3075241) (← links)
- Formalising Overlap Algebras in Matita (Q3094175) (← links)
- Type classes for mathematics in type theory (Q3094177) (← links)
- (Q3116967) (← links)
- Hints in Unification (Q3183522) (← links)
- Packaging Mathematical Structures (Q3183538) (← links)
- A Certified Study of a Reversible Programming Language (Q4580228) (← links)
- A User Interface for a Mathematical System that Allows Ambiguous Formulae (Q5166498) (← links)
- An Interactive Driver for Goal-directed Proof Strategies (Q5166499) (← links)
- A User-friendly Interface for a Lightweight Verification System (Q5170234) (← links)
- Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit (Q5170238) (← links)
- (Q5195246) (← links)
- (Q5195248) (← links)
