Skip to main content
padlock icon - secure page this page is secure

Open Access The European research network on types for programming and verification

Download Article:
 Download
(PDF 194.2 kb)
 
Types are pervasive in programming and information technology. A type defines a formal interface between software components, allowing the automatic verification of their connections, and greatly enhancing the robustness and reliability of computations and communications. In rich dependent type theories, the full functional specification of a program can be expressed as a type. Type systems have rapidly evolved over the past years, becoming more sophisticated, capturing new aspects of the behaviour of programs and the dynamics of their execution.

This COST Action will give a strong impetus to research on type theory and its many applications in computer science, by promoting (1) the synergy between theoretical computer scientists, logicians and mathematicians to develop new foundations for type theory, for example as based on the recent development of "homotopy type theory'', (2) the joint development of type theoretic tools as proof assistants and integrated programming environments, (3) the study of dependent types for programming and its deployment in software development, (4) the study of dependent types for verification and its deployment in software analysis and verification. The action will also tie together these different areas and promote cross-fertilisation.

Europe has a strong type theory community, ranging from foundational research to applications in programming languages, verification and theorem proving, which is in urgent need of better networking. A COST Action that crosses the borders will support the collaboration between groups and complementary expertise, and mobilise a critical mass of existing type theory research.
No References for this article.
No Supplementary Data.
No Article Media
No Metrics

Keywords: Automatic verification; Homotopy type theory; Software development; Thype theoretic tools; Type theory; Verification

Document Type: Research Article

Publication date: June 1, 2017

More about this publication?
  • Impact is a series of high-quality, open access and free to access science reports designed to enable the dissemination of research impact to key stakeholders. Communicating the impact and relevance of research projects across a large number of subjects in a content format that is easily accessible by an academic and stakeholder audience. The publication features content from the world's leading research councils, policy groups, universities and research projects. Impact is published under a CC-BY Creative Commons licence.

  • Subscribe to this Title
  • Terms & Conditions
  • Disseminating research in Impact
  • Information about Impact
  • Ingenta Connect is not responsible for the content or availability of external websites
  • Access Key
  • Free content
  • Partial Free content
  • New content
  • Open access content
  • Partial Open access content
  • Subscribed content
  • Partial Subscribed content
  • Free trial content
Cookie Policy
X
Cookie Policy
Ingenta Connect website makes use of cookies so as to keep track of data that you have filled in. I am Happy with this Find out more