Matita
From MaRDI portal
Cited in
(only showing first 100 items - show all)- PCM library
- finmap
- Proviola
- Aligning concepts across proof assistant libraries
- foaf
- LAD
- Proof General
- From types to sets by local type definition in higher-order logic
- TeXmacs
- GtkMathView
- jsMath
- HOL-Omega
- C-CoRN
- NNexus
- Formal metatheory of programming languages in the Matita interactive theorem prover
- STEX+
- Polar
- KAT-ML
- Formulator MathML
- Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean}
- From the universality of mathematical truth to the interoperability of proof systems
- Coq/SSReflect
- Proof General Kit
- Epigram
- Agda
- Irdis
- CtCoq
- ProofWeb
- GUItar
- PDCoq
- Paco
- The Coq library as a theory graph
- A plugin to export Coq libraries to XML
- Deciding Kleene algebra terms equivalence in Coq
- Towards semantic mathematical editing
- A canonical locally named representation of binding
- RATH-Agda
- Declarative representation of proof terms
- Procedural representation of CIC proof terms
- Crystal: Integrating structured queries into a tactic language
- A study on fractional differential equations using the fractional Fourier transform
- CLPGUI
- Lean
- Congruence closure in intensional type theory
- From types to sets by local type definitions in higher-order logic
- Incompleteness, Undecidability and Automated Proofs
- Tinycals: step by step tacticals
- Reverse complexity
- Asynchronous user interaction and tool integration in Isabelle/PIDE
- A bi-directional refinement algorithm for the calculus of (co)inductive constructions
- A Web Interface for Matita
- A Compact Proof of Decidability for Regular Expression Equivalence
- A Language of Patterns for Subterm Selection
- Formalizing Turing Machines
- A formal proof of Borodin-Trakhtenbrot's gap theorem
- HOL Zero
- Computational Complexity Via Finite Types
- Foundational extensible corecursion: a proof assistant perspective
- Friends with benefits. Implementing corecursion in foundational proof assistants
- On choice rules in dependent type theory
- Menhir
- The swap of integral and limit in constructive mathematics
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- Theseus
- Formalising overlap algebras in Matita
- Type classes for mathematics in type theory
- CoqMTU
- Enabling collaboration on semiformal mathematical knowledge by semantic web integration
- Plat-Omega
- NetSketch
- Hints in Unification
- Packaging Mathematical Structures
- scunac
- CoCaml
- The Lean theorem prover (system description)
- scientific article; zbMATH DE number 5587007 (Why is no real title available?)
- A constructive and formal proof of Lebesgue's dominated convergence theorem in the interactive theorem prover Matita
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- RedPRL
- Oz Explorer
- The CADE-22 automated theorem proving system competition -- CASC-22
- Proviola: a tool for proof re-animation
- Crafting a Proof Assistant
- Natural Deduction Environment for Matita
- About the Formalization of Some Results by Chebyshev in Number Theory
- HOLCF
- ELPI
- Towards ``mouldable code via nested code graph transformation
- APT
- Whelp
- Heq
- A certified study of a reversible programming language
- cart-cube
- Recycling proof patterns in Coq: case studies
- Type classes for efficient exact real arithmetic in \textsc{Coq}
- The strategy challenge in SMT solving
- Superposition as a logical glue
- Dot-types and their implementation
- Validating Mathematical Structures
- Programming and Proving with Classical Types
This page was built for software: Matita
