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
Copyright 2001-2017 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.

Яндекс.Метрика