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 53 articles , 2 standard articles )

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

1 2 3 next

  1. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  2. Maietti, Maria Emilia: On choice rules in dependent type theory (2017)
  3. Blanqui, Frédéric: Termination of rewrite relations on $\lambda$-terms based on Girard’s notion of reducibility (2016)
  4. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definitions in higher-order logic (2016)
  5. Selsam, Daniel; de Moura, Leonardo: Congruence closure in intensional type theory (2016)
  6. Asperti, Andrea: Computational complexity via finite types (2015)
  7. Asperti, Andrea: Reverse complexity (2015)
  8. Asperti, Andrea; Ricciotti, Wilmer: A formalization of multi-tape Turing machines (2015)
  9. de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob: The Lean theorem prover (system description) (2015)
  10. Fridlender, Daniel; Pagano, Miguel: Pure type systems with explicit substitutions (2015)
  11. Moreira, Nelma; Pereira, David; Melo de Sousa, Simão: Deciding Kleene algebra terms equivalence in Coq (2015)
  12. van der Hoeven, Joris: Towards semantic mathematical editing (2015)
  13. Heras, Jónathan; Komendantskaya, Ekaterina: Recycling proof patterns in Coq: case studies (2014)
  14. Kahl, Wolfram: Towards “mouldable code” via nested code graph transformation (2014)
  15. de Moura, Leonardo; Passmore, Grant Olney: The strategy challenge in SMT solving (2013)
  16. Krebbers, Robbert; Spitters, Bas: Type classes for efficient exact real arithmetic in Coq (2013)
  17. Asperti, Andrea: A compact proof of decidability for regular expression equivalence (2012)
  18. Asperti, Andrea; Ricciotti, Wilmer: A web interface for Matita (2012)
  19. Asperti, Andrea; Ricciotti, Wilmer: Formalizing Turing machines (2012)
  20. Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico: Formal metatheory of programming languages in the Matita interactive theorem prover (2012)

1 2 3 next