Tags : Browse Projects

Select a tag to browse associated projects and drill deeper into the tag cloud.

Isabelle

Analyzed 4 months ago

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle is developed at University of Cambridge (Larry Paulson) and Technical University of Munich (Tobias Nipkow).

312K lines of code

17 current contributors

over 5 years since last commit

2 users on Open Hub

Activity Not Available

I Use This

Mostly written in OCaml

Licenses: BSD-3-Clause

Tags logic math proof proof_assistant

seL4

Analyzed 6 months ago

The seL4 microkernel The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement.

1.04M lines of code

58 current contributors

6 months since last commit

2 users on Open Hub

Activity Not Available

I Use This

Mostly written in C

Licenses: GNU_Gener...

Tags haskell isabelle l4 microkernel os proof sel4 verification

iron lambda

I

Analyzed 4 months ago

Coq formalizations of functional languages

39.7K lines of code

0 current contributors

almost 5 years since last commit

0 users on Open Hub

Activity Not Available

I Use This

Mostly written in coq

Licenses: No declared licenses

Tags coq functional functional_language language mathematics proof research theorem typetheory