Category theory and verification

[Ivan Tarasov]

А есть какая-нибудь связь между теорией категорий и верификацией программ?

Иван

[Daniil Elovkov]

Ivan Tarasov wrote:
> А есть какая-нибудь связь между теорией категорий и верификацией программ?
>

Привет

Мне кажется, что мягко говоря очень опосредованная. Т.е. по-моему нету.

Я мало понимаю в теории категорий, но вроде ее можно привязать к чему угодно, поэтому какую-то связь с каким-нибудь из методов верификации наверно можно соорудить... :)

Но вопрос, правда, очень общий, согласись.

--
Daniil Elovkov

[Yakov ZAYTSEV]

есть связь между конструктивным доказательством и верификацией, а уж
для построения таких программ, конечно, аппарат ТК пригодится ;-)

2009/10/5 Daniil Elovkov <daniil....@googlemail.com>:

--
Best wishes,
Y

[Daniil Elovkov]

В принципе это я и имел в виду, когда говорил "очень опосредованная" :)

--
Daniil Elovkov

[Alexander Vlasov]

> А есть какая-нибудь связь между теорией категорий и верификацией программ?

Есть тесная связь между теорией типов и верификацией программ.
Теория категорий, по крайней мере, монады, весьма полезна для
верификации императивных программ, потому как верификация лучше
развита для чистых функциональных программ. А в чистом функ языке
можно инкапсулировать императивность внутри монады. Соответственно,
можно верифицировать императивные программы путем верификации
соответствующих конструкций с использованием монад.

[Yakov ZAYTSEV]

можно proof link?

2009/11/9 Alexander Vlasov <glav...@gmail.com>:

--
Best wishes,
Y

[Alexander Vlasov]

> можно proof link?
Ну вот к примеру пример подхода: императивные монады в HOL
http://web.cecs.pdx.edu/~jmatthew/papers/TPHOLs08.pdf