Matita (that means pencil in italian) is an experimental, interactive theorem prover under development at the Computer Science Department of the University of Bologna. An interactive prover is a software tool aiding the development of formal proofs by man-machine collaboration. It provides a formal language where mathematical definitions, executable algorithms and theorems cohexist, and an interactive environment keeping the current status of the proof, and updating it according to commands (usually called tactics) issued by the user.

References in zbMATH (referenced in 39 articles , 2 standard articles )

Showing results 1 to 20 of 39.
Sorted by year (citations)

1 2 next

  1. Blanqui, Frédéric: Termination of rewrite relations on $\lambda$-terms based on Girard’s notion of reducibility (2016)
  2. Asperti, Andrea: Reverse complexity (2015)
  3. Asperti, Andrea; Ricciotti, Wilmer: A formalization of multi-tape Turing machines (2015)
  4. de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob: The Lean theorem prover (system description) (2015)
  5. Moreira, Nelma; Pereira, David; Melo de Sousa, Simão: Deciding Kleene algebra terms equivalence in Coq (2015)
  6. van der Hoeven, Joris: Towards semantic mathematical editing (2015)
  7. Heras, Jónathan; Komendantskaya, Ekaterina: Recycling proof patterns in Coq: case studies (2014)
  8. Kahl, Wolfram: Towards “mouldable code” via nested code graph transformation (2014)
  9. Krebbers, Robbert; Spitters, Bas: Type classes for efficient exact real arithmetic in Coq (2013)
  10. Asperti, Andrea: A compact proof of decidability for regular expression equivalence (2012)
  11. Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico: Formal metatheory of programming languages in the Matita interactive theorem prover (2012)
  12. Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico: A bi-directional refinement algorithm for the calculus of (co)inductive constructions (2012)
  13. Gonthier, Georges; Tassi, Enrico: A language of patterns for subterm selection (2012)
  14. Lapets, Andrei; Kfoury, Assaf: A user-friendly interface for a lightweight verification system (2012)
  15. Wenzel, Makarius: Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit (2012)
  16. Xue, Tao; Luo, Zhaohui: Dot-types and their implementation (2012)
  17. Asperti, Andrea; Maietti, Maria Emilia; Sacerdoti Coen, Claudio; Sambin, Giovanni; Valentini, Silvio: Formalization of formal topology by means of the interactive theorem prover Matita (2011)
  18. Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico: The Matita interactive theorem prover (2011)
  19. Lange, Christoph: Enabling collaboration on semiformal mathematical knowledge by semantic web integration (2011)
  20. Spitters, Bas; van der Weegen, Eelis: Type classes for mathematics in type theory (2011)

1 2 next