Types for Proofs and Programs

The aim of the research is to develop the technology of formal reasoning and computer programming based on Type Theory. This is done by improving the languages and computerised tools for reasoning, and by applying the technology in several domains such as analysis of programming languages, certified software, formalisation of mathematics and mathematics education.

Research activities

Participants


More information : http://www.cs.chalmers.se/Cs/Research/Logic/Types/