Matita (means pencil in italian) is an experimental, interactive theorem prover.
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.
Matita is based on a Dependent Type System known as the Calculus of Inductive Constructions.
It embeds key computational constructs of functional programming languages: functions can be defined by (well-founded) recursion, and are live entities that can be tested and executed.
At the same time, proofs are an integrated part of the formalism, allowing, via the Curry Howard isomorphism, a smooth interplay between specification, implementation and verification: proofs are objects of the language, and can be treated as normal data, naturally leading to a programming style akin to proof-carrying-code, where chunks of software come equipped with proofs of (some of) their properties.
Matita is part of HELM, an Hypertextual, Electronic Library of Mathematics, developed at the Computer Science Department, University of Bologna, Italy.
Developer: Andrea Asperti, Ferruccio Guidi, Luca Padovani, Enrico Tassi, Claudio Sacerdoti Coen, and Stefano Zacchiroli
License: GNU General Public License Version 2.0
|New to Linux? Read our Linux for Starters series. We start right at the basics and teach you everything you need to know to get started with Linux.|
|The largest compilation of the best free and open source software in the universe. Each article is supplied with a legendary ratings chart helping you to make informed decisions.|
|Hundreds of in-depth reviews offering our unbiased and expert opinion on software. We offer helpful and impartial information.|
|Replace proprietary software with open source alternatives: Google, Microsoft, Apple, Adobe, IBM, Autodesk, Oracle, Atlassian, Corel, Cisco, Intuit, and SAS.|
|Linux Around The World showcases events and usergroups that are relevant to Linux enthusiasts.|
|Surveys popular streaming services from a Linux perspective: Amazon Music Unlimited, Myuzi, Spotify, Deezer, Tidal.|
|Saving Money with Linux looks at how you can reduce your energy bills running Linux.|
|Essential Linux system tools focuses on small, indispensable utilities, useful for system administrators as well as regular users.|
|Linux utilities to maximise your productivity. Small, indispensable tools, useful for anyone running a Linux machine.|
|Home computers became commonplace in the 1980s. Emulate home computers including the Commodore 64, Amiga, Atari ST, ZX81, Amstrad CPC, and ZX Spectrum.|
|Now and Then examines how promising open source software fared over the years. It can be a bumpy ride.|
|Linux at Home looks at a range of home activities where Linux can play its part, making the most of our time at home, keeping active and engaged.|
|Linux Candy reveals the lighter side of Linux. Have some fun and escape from the daily drudgery.|
|Getting Started with Docker helps you master Docker, a set of platform as a service products that delivers software in packages called containers.|
|Best Free Android Apps. We showcase free Android apps that are definitely worth downloading. There's a strict eligibility criteria for inclusion in this series.|
|These best free books accelerate your learning of every programming language. Learn a new language today!|
|These free tutorials offer the perfect tonic to our free programming books series.|
|Stars and Stripes is an occasional series looking at the impact of Linux in the USA.|