VERIFICATION OF REACTIVE PROGRAMS BY DEPENDENT TYPE SYSTEMS WITH STRUCTURAL INDUCTION

Yan Malakhovski, Georgiy Korneev

2012 , VOLUME 12, NUMBER 6 ( November-December )

ISSN 2226-1494 (print), ISSN 2500-0373 (online)

Publications

Editor-in-Chief

Nikiforov
Vladimir O.
D.Sc., Prof.

Partners

VERIFICATION OF REACTIVE PROGRAMS BY DEPENDENT TYPE SYSTEMS WITH STRUCTURAL INDUCTION

Y. Malakhovski, G. Korneev

Read the full article

Abstract

The article is devoted to a constructive proof (in Agda programming language) of the fact that Boolean formula satisfiability problem by means of sequent calculus and verification with CTL specifications can be implemented as structurally recursive dependently typed functions.

Keywords: Boolean formula satisfiability problem, verification, functional programming, type systems, dependent types

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License