Matita
From MaRDI portal
Software:18274
swMATH6140MaRDI QIDQ18274FDOQ18274
Author name not available (Why is that?)
Cited In (73)
- The swap of integral and limit in constructive mathematics
- Natural Deduction Environment for Matita
- Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems
- A User-friendly Interface for a Lightweight Verification System
- Validating Mathematical Structures
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita
- Hints in Unification
- Programming and Proving with Classical Types
- From types to sets by local type definition in higher-order logic
- From the universality of mathematical truth to the interoperability of proof systems
- Towards ``mouldable code via nested code graph transformation
- Title not available (Why is that?)
- Spurious disambiguation errors and how to get rid of them
- Type classes for mathematics in type theory
- Friends with Benefits
- About the Formalization of Some Results by Chebyshev in Number Theory
- Aligning concepts across proof assistant libraries
- Title not available (Why is that?)
- Title not available (Why is that?)
- Isabelle as Document-Oriented Proof Assistant
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- The Lean Theorem Prover (System Description)
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
- Reverse complexity
- Computational Complexity Via Finite Types
- Proviola: A Tool for Proof Re-animation
- Towards semantic mathematical editing
- From Types to Sets by Local Type Definitions in Higher-Order Logic
- A formalization of multi-tape Turing machines
- On Choice Rules in Dependent Type Theory
- Pure type systems with explicit substitutions
- A canonical locally named representation of binding
- Declarative representation of proof terms
- Crystal: Integrating structured queries into a tactic language
- Procedural representation of CIC proof terms
- A Formal Proof of Borodin-Trakhtenbrot’s Gap Theorem
- Title not available (Why is that?)
- A Compact Proof of Decidability for Regular Expression Equivalence
- Title not available (Why is that?)
- A Language of Patterns for Subterm Selection
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- A Certified Study of a Reversible Programming Language
- Type classes for efficient exact real arithmetic in Coq
- Tinycals: step by step tacticals
- Recycling proof patterns in Coq: case studies
- Tactics for hierarchical proof
- Packaging Mathematical Structures
- Incompleteness, Undecidability and Automated Proofs
- Deciding Kleene algebra terms equivalence in Coq
- Formalising Overlap Algebras in Matita
- Formal metatheory of programming languages in the Matita interactive theorem prover
- Title not available (Why is that?)
- Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
- Implementing type theory in higher order constraint logic programming
- Crafting a Proof Assistant
- A plugin to export Coq libraries to XML
- The Coq library as a theory graph
- Congruence Closure in Intensional Type Theory
- A User Interface for a Mathematical System that Allows Ambiguous Formulae
- Preface
- Foundational extensible corecursion: a proof assistant perspective
- Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit
- A Web Interface for Matita
- Formalizing Turing Machines
- The Strategy Challenge in SMT Solving
- An Interactive Driver for Goal-directed Proof Strategies
- A study on fractional differential equations using the fractional Fourier transform
- Dot-types and Their Implementation
- Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean}
- The CADE-22 automated theorem proving system competition – CASC-22
- A bi-directional refinement algorithm for the calculus of (co)inductive constructions
This page was built for software: Matita
