This project studies new dependently typed systems suitable for the development and mechanization of programming language semantics. Particular emphasis is given to languages supporting concurrency and non-determinism, such as transition systems and process calculi. Popular proof assistants based on dependent type theory, such as Agda and Coq, are inadequate for the formal verification of the denotational semantics of such languages because of their insufficiently expressive type systems. We address this issue by extending modern type-theoretic frameworks, such as homotopy type theory, with a new class of coinductive types coming from final coalgebras of accessible functors. In denotational semantics, these types are necessary for handling the non-deterministic and continuously-interactive behavior of processes. The resulting more expressive type systems will prove themselves capable of encoding the formal semantics of various languages with concurrency and non-determinism.
The central research focus of the technology and economics of trust in software theme will be certified software. Topics of research include:
• methods and tools for certification of software; program analysis, transformation, generation; in particular for big data, cloud and IoT;
• static analysis (model checkers, theorem provers), verification, systematic testing;
• contract languages, languages with powerful type systems (refinement types, dependent types); domain-specific languages;
• program synthesis and program learning, program understanding;
• repositories of certified software, evolution of certified software;
• trust in closed-source software, gradual trust-building;
• trading trust, pricing of trust, game theory of trust.