Библиотеки, написанные на Isabelle

l4v

Спецификация seL4 и доказательства.
  • 464
  • GNU General Public License v3.0

marlowe

Реализация прототипа предметно-ориентированного языка для разработки смарт-контрактов в криптовалютах.
  • 164
  • Apache License 2.0

cogent

Когент проект.
  • 154
  • GNU General Public License v3.0

tangentlabs

множество мини-экспериментов на разных языках.
  • 38

sortnetopt

Нижние границы размера для сортирующих сетей.
  • 38

WasmCert-Isabelle

Механизация Wasm в Isabelle..
  • 17
  • BSD 2-clause "Simplified"

isabelle-lambda-calculus

Формальное определение и проверка системы F. Будет распространена на систему Fc.
  • 8

Lambda-RAM-Compiler

  • 2

ouroboros-high-assurance

Высоконадежная реализация семейства протоколов Ouroboros.
  • 0
  • GNU General Public License v3.0