Languages Features Calendar CSV Lists Blog About Sponsor Add Language
GitHub icon



< >

Matita is a programming language created in 1999.

#2196on PLDB 23Years Old 70Users
0Books 1Papers

Matita is an experimental proof assistant under development at the Computer Science Department of the University of Bologna. It is a tool aiding the development of formal proofs by man-machine collaboration, providing a programming environment where formal specifications, executable algorithms and automatically verifiable correctness certificates naturally coexist. Matita is based on a dependent type System known as the Calculus of (Co)Inductive Constructions (a derivative of Calculus of Constructions), and is compatible, to some extent, with Coq. Read more on Wikipedia...

Publications about Matita from Semantic Scholar

title authors year citations influentialCitations
Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover A. Asperti and W. Ricciotti and C. Coen and E. Tassi 2012 6 0
npl-lang.html 路 matita.html 路 mama-software.html

View source

PLDB - Build the next great programming language 路 v2022 Day 93 Docs Build Acknowledgements Traffic Today Traffic Trends Mirrors GitHub