Интернет магазин китайских планшетных компьютеров

Компьютеры - Coq - Библиотеки и приложения

• Формализация различных разделов математики:
  • Абстрактная алгебра
  • Арифметика и теория чисел
  • Геометрия
  • Комбинаторика
  • Лямбда-исчисление
  • Математическая логика, включая само исчисление конструкций и Pure Type Systems
  • Математический анализ
  • Теория графов, включая доказательство существования решения проблемы четырёх красок — «доказательство практически невозможно проверить, не используя компьютер»
  • Теория категорий
  • Теория множеств, классическая и интуиционистская
  • Формальные языки и автоматы
• И информатики:
  • Семантика языков программирования
  • Корректность алгоритмов RSA, алгоритма Хаффмана и других
  • Параллельные системы и протоколы
  • Логические игры
• Верификация программ:
  • Why — платформа для верификации программ, которая используется в:
    • Krakatoa — инструмент для верификации программ на языках программирования Java/Java Card, аннотированных с помощью Java Modeling Language
    • Frama-C — инструмент для верификации программ на Си
  • Ynot — библиотека для верификации императивных программ. Использует развитие монады IO, логику Хоара, сепарационную логику