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

Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Copyright 2001-2024 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.

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