The concept of proof in the context of a type-theoretic approach, I: Proof of computer program correctness

Research output: Contribution to journalArticleResearchpeer-review

Abstract

Рассматривается теоретико-типовое понятие доказательства корректности компьютерных программ. Исследуются особенности этого понятия, а также ряд связанных с ним теоретико-познавательных проблем. Особое внимание уделяется проблеме обозримости и связи априорного и апостериорного. Настоящая статья является первой в серии о понятии теоретико-типового доказательства.
Translated title of the contributionThe concept of proof in the context of a type-theoretic approach, I: Proof of computer program correctness
Original languageRussian
Pages (from-to)49-57
JournalВестник Томского государственного университета. Философия. Социология. Политология.
Issue number46
DOIs
Publication statusPublished - 2018

Fingerprint

Program Correctness
Formal Proof
Proof of correctness
Categorical
Context
Concepts
Type Inference
Information Hiding

WoS ResearchAreas Categories

  • Social Sciences, Interdisciplinary

GRNTI

  • 02.00.00 PHILOSOPHY

Level of Research Output

  • VAK List

Cite this

@article{bf973039948c40eda8d4fc3792f02da4,
title = "ПОНЯТИЕ ДОКАЗАТЕЛЬСТВА В КОНТЕКСТЕ ТЕОРЕТИКО-ТИПОВОГО ПОДХОДА, I: ДОКАЗАТЕЛЬСТВО ПРОГРАММ",
abstract = "Рассматривается теоретико-типовое понятие доказательства корректности компьютерных программ. Исследуются особенности этого понятия, а также ряд связанных с ним теоретико-познавательных проблем. Особое внимание уделяется проблеме обозримости и связи априорного и апостериорного. Настоящая статья является первой в серии о понятии теоретико-типового доказательства.",
author = "Ламберов, {Лев Дмитриевич}",
year = "2018",
doi = "10.17223/1998863Х/46/6",
language = "Русский",
pages = "49--57",
journal = "Вестник Томского государственного университета. Философия. Социология. Политология.",
issn = "1998-863X",
publisher = "Национальный исследовательский Томский государственный университет",
number = "46",

}

TY - JOUR

T1 - ПОНЯТИЕ ДОКАЗАТЕЛЬСТВА В КОНТЕКСТЕ ТЕОРЕТИКО-ТИПОВОГО ПОДХОДА, I: ДОКАЗАТЕЛЬСТВО ПРОГРАММ

AU - Ламберов, Лев Дмитриевич

PY - 2018

Y1 - 2018

N2 - Рассматривается теоретико-типовое понятие доказательства корректности компьютерных программ. Исследуются особенности этого понятия, а также ряд связанных с ним теоретико-познавательных проблем. Особое внимание уделяется проблеме обозримости и связи априорного и апостериорного. Настоящая статья является первой в серии о понятии теоретико-типового доказательства.

AB - Рассматривается теоретико-типовое понятие доказательства корректности компьютерных программ. Исследуются особенности этого понятия, а также ряд связанных с ним теоретико-познавательных проблем. Особое внимание уделяется проблеме обозримости и связи априорного и апостериорного. Настоящая статья является первой в серии о понятии теоретико-типового доказательства.

UR - https://elibrary.ru/item.asp?id=36818406

UR - https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=tsmetrics&SrcApp=tsm_test&DestApp=WOS_CPL&DestLinkType=FullRecord&KeyUT=000461487800006

U2 - 10.17223/1998863Х/46/6

DO - 10.17223/1998863Х/46/6

M3 - Статья

SP - 49

EP - 57

JO - Вестник Томского государственного университета. Философия. Социология. Политология.

JF - Вестник Томского государственного университета. Философия. Социология. Политология.

SN - 1998-863X

IS - 46

ER -