annenkov Goto Github PK

2ltt-docker

A docker image for the two-level type theory formalisation in Lean

annenkov.github.io

awesome-coq

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]

ccd-redeem

certicoq

clvm

CL interpreter written in ConCert

compiler

Compiler for Elm, a functional language for reliable webapps.

concert

A framework for smart contract verification in Coq

concert-testing-examples

Example usage of ConCert's property-based testing framework, on various smart contracts

concordium-contracts-common

Common functionality used by smart contracts and the host environment on the Concordium blockchain.

concordium-marlowe

Marlowe interpreter and contract manager

concordium-rust-smart-contracts

Standard library for writing smart contracts for the Concordium blockchain.

contracts

Symbolic financial contract EDSL

coq-sprop-opam

A package for a version of Coq supporting SProp

coq.sprop

A fork of https://github.com/SkySkimmer/coq which is compatible with Template Coq with SProp

cropzoom

dataflow-samples

Some examples of dataflow analysis

diffgeo

A formalization of synthetic differential geometry in Coq using infinitesimal analysis

emacs.d

An Emacs configuration bundle with batteries included

entity-model

fmbc19-artefact

Coq development for FMBC'19

format

ACM consolidated LaTeX styles

fullcalendar

Fork of Full-sized drag & drop event calendar with Resource views (jQuery plugin) http://tux.fi/~jarnok/fullcalendar-resourceviews/ This fork adds "summary" column with own fetcher and renderer.

futhark-extract

Extracting Futhark code from the Coq proof assistant

haskell-bio

Some bioinformatics algorithms in Haskell

kure-examples

lbs

Supplementary materials for the Language-based Security Lecture on Smart Contracts

lean2

Lean theorem prover version 0.2 (it supports standard and HoTT modes)

log-monitoring

A parser and a web-interface for viewing/filtering logs implemented in Racket

model-structures-coq

Formalization of a model structure on the universe of Types in Coq