Matita

No author found.

Related Items (73)

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

This page was built for software: Matita