Journal
Scientific and technical journal of information technologies, mechanics and optics
UDK
Issue:6 (82)
Download PDF0 Kbyte
VERIFICATION OF REACTIVE PROGRAMS BY DEPENDENT TYPE SYSTEMS WITH STRUCTURAL INDUCTION
Annotation
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
Постоянный URL
Articles in current issue
- CAD FEATURES FOR DIFFRACTION GRATINGS MODELING
- ABERRATION ANALYSIS OF THE FINE OPTICAL COMPONENT COMPOSITION WITH CONCENTRIC MENISCUS
- MODERNIZED SOFTWARE COMPLEX FOR SYNTHESIS AND RECONSTRUCTION OF FRESNEL HOLOGRAMS-PROJECTORS
- SPATIAL POSITION DETERMINATION METHOD FOR THE OBJECT NEAR WATER SURFACE
- ROTATIONAL DEPENDENCE OF CORIOLIS AND FERMI TYPE RESONANCES IN SMALL LINEAR MOLECULES
- SPECIAL FEATURES OF ITERATION METHODS FOR PHASE PROBLEM IN OPTICS
- MANGANESE LUMINESCENCE IN FLUORINE-PHOSPHATE GLASSES
- ROBUSTNESS ANALYSIS OF THE ELECTRIC DRIVE NON-ADAPTIVE CONTROL SYSTEM WITH STRUCTURE AND PARAMETERS VARIATIONS
- ACCELEROMETER DATA SPECTRAL ANALYSIS FOR VEHICLES DETECTION AND IDENTIFICATION
- ANALYSIS OF LINEAR SYSTEMS WITH VARIABLE PARAMETERS FOR INTERVAL OBSERVER SYNTHESIS
- DVB-T FIELD MODELING IN URBAN AREAS
- DEEP-WATER THREE-AXIS TILT SENSORS APPLICATION IN SOLVING GEOTECHNICAL MONITORING TASKS
- VERIFICATION OF REACTIVE PROGRAMS BY DEPENDENT TYPE SYSTEMS WITH STRUCTURAL INDUCTION
- SIGNAL-TO-NOISE RATIO ESTIMATION ALGORITHM FOR SPEECH SIGNALS
- ANT COLONY OPTIMIZATION-BASED METHOD OF FINITE-STATE MACHINE INDUCTION
- C/C++ PROGRAMMING OF DISTORTED IMAGE RESTORATION PROBLEMS IN TEXAS INSTRUMENTS SIGNAL MICROPROCESSORS
- FINITE-STATE MACHINE IMPLEMENTATION OF EMBEDDED SYSTEM USER INTERFACE BASED ON ASPECT-ORIENTED DESCRIPTION
- HISTOGRAM NORMALIZATION OF SPEECH FEATURES FOR SPEAKERS’ VERIFICATION
- IDENTIFICATION SYSTEM OF THE SPEAKER’S AGE GROUP BY SPONTANEOUS SPEECH RECORD
- GENOME CONTIGS ASSEMBLY METHOD BASED ON DE BRUJIN GRAPHS AND OVERLAP GRAPHS
- LEAD-FLUORINE NANOGLASS CERAMIC INVESTIGATION DOPED WITH YTTRIUM AND NEODYMIUM IONS
- SOFTWARE MODULE FOR PARAMETERS ESTIMATING OF DISPERSE SYSTEMS BY THEIR IMAGES FOR QUANTITATIVE THREE-DIMENSIONAL STEREO ANALYSIS
- INFLUENCE OF FILLER SURFACE MODIFICATION ON LATEX FILMS PROPERTIES
- PRINCIPLES OF BRANCH SYSTEM CREATION FOR THE AUTOMATED DESIGN IN AVIATION INSTRUMENTATION
- CALCULATION OF THE MINIMUM PATH LENGTH WIRE IN THE PRINTED WIRING TOPOLOGICAL ROUTING
- ALGORITHM OF SPAM-BELONGING DEFINITION FOR DOCUMENTS ON THE BASIS OF FEJER DISPLAYS
- ANALYSIS OF INTERNET USER IDENTIFICATION METHODS
- DEPERSONALIZATION ALGORITHM OF PERSONAL INFORMATION
- ALGORITHM OF INDIVIDUALS’ DETAILS IDENTIFICATION IN THE DATABASES BY LEVENSTEIN METRIC
- ONTOLOGY DEVELOPMENT OF OPEN GOVERNMENT DATA ON EXAMPLE OF ST. PETERSBURG BUDGET EXPENDITURES
- X-RAY DIFFRACTION ANALYSIS OF OXIFLUORIDE NANOGLASS CERAMIC DOPED WITH YTTERBIUM AND ERBIUM
- METHOD OF FUNCTIONALITY EXPANSION OF MOBILE TERMINAL FOR MOBILE OBJECTS MONITORING
- RESEARCH OF AUTOCOLLIMATING ANGULAR DEFORMATION MEASUREMENT SYSTEM FOR LARGE-SIZE OBJECTS
- EXPERIMENTAL RESEARCH OF THE OPTICAL ELECTRONIC SYSTEM FOR DEFOR
- ORGANIZATION AND PLANNING OF THE INSTRUMENT-MAKING ENTERPRISE ACTIVITIES AT CARRYING OUT OF SCIENTIFIC-RESEARCH AND EXPERIMENTAL-DESIGN WORKS IN AVIATION
- STEREOSCOPIC OPTICAL ELECTRONIC SYSTEM FOR DEFORMATION MONITORING OF LARGE-SIZE DOME STRUCTURES