Главная Макинтош Регистрация


Приветствую Вас Гость | RSSВторник, 16.07.2019, 08:16
Наш опрос
Оцените мой сайт
Всего ответов: 3


Онлайн всего: 1
Гостей: 1
Пользователей: 0

Форма входа

Главная » 2013 » Октябрь » 8 » F*
http://research.microsoft.com/en-us/projects/fstar/: «F* is a new dependently typed language for secure distributed programming. It's designed to be enable the construction and communication of proofs of program properties and of properties of a program's environment in a verifiably secure way. F* compiles to .NET bytecode in type-preserving style, and interoperates smoothly with other .NET languages, including F%23, on which it is based. Self-certification of F*: We have verified the F* type checker using F* itself, using a novel bootstrapping technique called self-certification.» http://research.microsoft.com/apps/pubs/?id=141708: «We present F*, a full-fledged design and implementation of a new dependently typed language for secure distributed programming. Unlike prior languages, F* provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F* and controls their interaction. F* subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs partially mechanized in Coq) and logical consistency for F*.» Via nponeccop.
Просмотров: 272 | Добавил: admin | Рейтинг: 0.0/0
Всего комментариев: 0
Имя *:
Email *:
Код *:

«  Октябрь 2013  »

Архив записей

Copyright MyCorp © 2019Хостинг от uCoz