GitHub topics: isabelle

Repositories

jvanbruegge/binder_datatypes

A new foundational package for Isabelle/HOL that implements binding-aware datatypes

Language: Isabelle - Size: 31.7 MB - Last synced at: 2 days ago - Pushed at: 3 days ago - Stars: 4 - Forks: 0

jaalonso/jaalonso.github.io

Índice de repositorios.

Language: HTML - Size: 68.1 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 1 - Forks: 0

awesomo4000/awesome-provable

A curated set of links to formal methods involving provable code.

Size: 25.4 KB - Last synced at: 9 days ago - Pushed at: over 3 years ago - Stars: 202 - Forks: 10

seL4/l4v

seL4 specification and proofs

Language: Isabelle - Size: 93.9 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 537 - Forks: 109

inpefess/isabelle-client

A client for Isabelle server (https://isabelle.in.tum.de)

Language: TeX - Size: 7.5 MB - Last synced at: 9 days ago - Pushed at: about 1 month ago - Stars: 10 - Forks: 1

lukaskollmer/advent-of-code

Advent of Code solutions, in OCaml and (sometimes) Isabelle/HOL

Language: OCaml - Size: 429 KB - Last synced at: about 2 months ago - Pushed at: 4 months ago - Stars: 2 - Forks: 0

javierdiaz72/Finite_Map_Extras

Useful syntactic sugar, new operators and functions, and their associated lemmas for finite maps which currently are not present in the standard `Finite_Map` theory.

Language: Isabelle - Size: 5.86 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 1

diekmann/Iptables_Semantics

Verified iptables Firewall Ruleset Analysis

Language: Isabelle - Size: 10 MB - Last synced at: 16 days ago - Pushed at: 10 months ago - Stars: 97 - Forks: 13

tobias-rothmann/Polynomial-Commitment-Schemes

Formalizing Polynomial Commitment Schemes in the Interactive Theorem Prover Isabelle.

Language: Isabelle - Size: 4.16 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 10 - Forks: 0

nielstron/bplustrees

A Verified Imperative Implementation of B+-Trees in Isabelle

Language: Isabelle - Size: 3.5 MB - Last synced at: 13 days ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 0

dominique-unruh/afp

Git clone of official afp repositories

Language: Shell - Size: 707 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 1 - Forks: 0

runtime-monitoring/explanator2

Explanator2 is an online monitor that produces verdicts in the form of explanations for Metric Temporal Logic formulas.

Language: Isabelle - Size: 20 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 1 - Forks: 0

data61/PSL

Language: Isabelle - Size: 175 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 65 - Forks: 9

ThreeFx/isabelle.vim

NeoVim extension used in conjunction with coc-isabelle

Language: Vim script - Size: 400 KB - Last synced at: 4 months ago - Pushed at: almost 3 years ago - Stars: 6 - Forks: 1

BaseMax/IssabelWebservicePHP

ISSABEL simple API Restful JSON: Provide call history reports from Issabel for a Call center powered by PHP with a JSON web-service interface

Language: PHP - Size: 214 KB - Last synced at: 5 days ago - Pushed at: almost 3 years ago - Stars: 7 - Forks: 0

jaycech3n/Isabelle-HoTT

An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle

Language: Standard ML - Size: 405 KB - Last synced at: 28 days ago - Pushed at: over 2 years ago - Stars: 34 - Forks: 3

shangsuru/concrete-semantics

Solutions to the problems in the book Concrete Semantics by Gerwin Klein and Tobias Nipkow

Language: Isabelle - Size: 313 KB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

BraeWebb/adventofcode2020

Advent of Code 2020

Language: Isabelle - Size: 56.6 KB - Last synced at: about 1 year ago - Pushed at: about 3 years ago - Stars: 0 - Forks: 0

logicalhacking/Isabelle_DOF

Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting as well as formal development.

Language: Isabelle - Size: 73.2 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 2 - Forks: 1

SEL4PROJ/jormungand

Isabelle/HOL theories for the paper "Backwards and Forwards with Separation Logic".

Language: Isabelle - Size: 26.6 MB - Last synced at: about 1 year ago - Pushed at: over 6 years ago - Stars: 2 - Forks: 0

appliedfm/growth-data

Measuring the growth of open source formal methods

Language: Python - Size: 36.6 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 4 - Forks: 0

SSoelvsten/cadiar 📦

Formal verification of the Adiar BDD package

Language: Isabelle - Size: 53.7 KB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0

uqcyber/veriopt-releases

Verifying the optimization phases of the GraalVM compiler

Language: Isabelle - Size: 63.8 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 11 - Forks: 1

supleed2/ELEC70056-HSV-CW1

About Coursework 1 for ELEC70056: Hardware and Software Verification, Software Component - Verification of code using Dafny and the theorem-prover Isabelle

Language: Isabelle - Size: 10.8 MB - Last synced at: 12 months ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

jaalonso/Calculemus

Ejercicios de demostración con Lean e Isabelle/HOL.

Language: Lean - Size: 4.24 MB - Last synced at: 25 days ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

isabelle-utp/utp-main

An implementation of Hoare and He's Unifying Theories of Programming in Isabelle

Language: Isabelle - Size: 155 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 34 - Forks: 9

dominique-unruh/scala-isabelle

A Scala library for controlling/interacting with Isabelle

Language: Scala - Size: 1.21 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 32 - Forks: 8

input-output-hk/equivalence-reasoner

An automated equivalence reasoner for Isabelle/HOL

Language: Isabelle - Size: 57.6 KB - Last synced at: about 1 month ago - Pushed at: about 1 year ago - Stars: 2 - Forks: 4

chrisdalvit/zeckendorf-theorem

A formal proof of the Zeckendorf theorem in Isabelle/HOL

Language: TeX - Size: 27.4 MB - Last synced at: 2 months ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 0

seanpm2001/AI2001_Category-Source_Code-SC-Isabelle

🧠️🖥️2️⃣️0️⃣️0️⃣️1️⃣️💾️📜️ The sourceCode:Isabelle category for AI2001, containing Isabelle programming language datasets

Language: R - Size: 2.46 MB - Last synced at: 7 days ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 1

rohitdureja/isabelle-practice

Exercises from the Prog-Prove manual of Isabelle

Language: Isabelle - Size: 22.5 KB - Last synced at: about 1 year ago - Pushed at: almost 7 years ago - Stars: 7 - Forks: 2

ekarayel/frequency_moments

Formal verification of randomized streaming algorithms for frequency moments.

Language: TeX - Size: 11.3 MB - Last synced at: over 1 year ago - Pushed at: about 2 years ago - Stars: 0 - Forks: 0

nunchaku-inria/nunchaku

Model finder for higher-order logic

Language: OCaml - Size: 3.98 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 41 - Forks: 3

eownerdead/verilambda

De Bruijn Index Lambda Calculus in Isabelle.

Language: Isabelle - Size: 6.84 KB - Last synced at: about 2 months ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

carlinmack/afp

Language: HTML - Size: 247 MB - Last synced at: over 1 year ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 0

Pinpickle/matapaki-lang

Alternative EVM smart contract language

Language: Isabelle - Size: 239 KB - Last synced at: over 1 year ago - Pushed at: almost 7 years ago - Stars: 3 - Forks: 0

isabelle-prover/inductive_sledgehammer

ATMEGA32U4 code for the physical Sledgehammer device developed at TUM

Language: C++ - Size: 471 KB - Last synced at: over 1 year ago - Pushed at: about 7 years ago - Stars: 1 - Forks: 0

jeltsch/actions-isabelle-build

GitHub action for building Isabelle sessions

Size: 10.7 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0

ThomasHickman/Isabelle-CAS-Integration

A project to integrate the functionality of Computer Algebra Systems into Isabelle

Language: Isabelle - Size: 124 KB - Last synced at: 16 days ago - Pushed at: almost 4 years ago - Stars: 3 - Forks: 2

adbrucker/isabelle-hacks

A Collection of Isabelle Programming Hacks

Language: Standard ML - Size: 393 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 2 - Forks: 1

larsrh/libisabelle-example 📦

Example project using libisabelle (DISCONTINUED)

Language: Scala - Size: 5.86 KB - Last synced at: about 2 years ago - Pushed at: almost 8 years ago - Stars: 0 - Forks: 0

larsrh/phd-thesis 📦

LaTeX sources of my PhD thesis (ARCHIVED)

Language: TeX - Size: 2.72 MB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 2 - Forks: 0

larsrh/afp 📦

sbt build of the Archive of Formal Proofs (DISCONTINUED)

Language: Scala - Size: 35.2 KB - Last synced at: almost 2 years ago - Pushed at: almost 6 years ago - Stars: 2 - Forks: 0

larsrh/multi-isabelle 📦

Conditional Isabelle/ML execution depending on Isabelle version (DISCONTINUED)

Language: Standard ML - Size: 16.6 KB - Last synced at: almost 2 years ago - Pushed at: almost 6 years ago - Stars: 0 - Forks: 0

larsrh/classy 📦

Type classes for Isabelle/ML (DISCONTINUED)

Language: Standard ML - Size: 36.1 KB - Last synced at: about 2 years ago - Pushed at: almost 6 years ago - Stars: 1 - Forks: 0

larsrh/purely-experimental 📦

Experiments in Isabelle/Pure (and a bit of HOL) (ARCHIVED)

Language: Standard ML - Size: 13.7 KB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 3 - Forks: 0

m-fleury/isabelle-snippets 📦

Snippets for Isabelle/VSCode

Language: Perl - Size: 19.5 KB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 0 - Forks: 0

larsrh/isabelle-cakeml 📦

Exporting CakeML to Isabelle with Lem (DISCONTINUED)

Language: Isabelle - Size: 274 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0

larsrh/libisabelle 📦

A Scala library which talks to Isabelle (DISCONTINUED)

Language: Scala - Size: 1.66 MB - Last synced at: almost 2 years ago - Pushed at: over 4 years ago - Stars: 38 - Forks: 8

jaycech3n/Isabelle-Spartan 📦

A dependent type theory logic for Isabelle

Language: Standard ML - Size: 361 KB - Last synced at: almost 2 years ago - Pushed at: about 4 years ago - Stars: 6 - Forks: 1

kappelmann/SpecCheck 📦

QuickCheck-like testing framework for Isabelle/ML

Language: Standard ML - Size: 268 KB - Last synced at: about 2 years ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 0

agomezl/simp-isar-mode 📦

A simple emacs mode for Isabelle (.thy) files

Language: Emacs Lisp - Size: 43.9 KB - Last synced at: over 1 year ago - Pushed at: about 8 years ago - Stars: 1 - Forks: 2

Related Keywords

isabelle 70 isabelle-hol 13 interactive-theorem-proving 6 proof-assistant 6 hol 5 formal-verification 5 verification 5 theorem-proving 4 proof 3 formal-methods 3 scala 3 lean 3 coq 3 ocaml 3 utp 2 type-theory 2 semantics 2 txt 2 neovim 2 logic 2 itp 2 artificial-intelligence 2 formal-proofs 2 cakeml 2 functional-programming 2 haskell 2 agda 2 gpl3 2 idris 2 gplv3 2 isabelle-language 2 md 2 maxima 1 wolfram-engine 1 fricas 1 cas 1 github-actions 1 sml 1 atmega32u4 1 sbt 1 sagemath 1 sympy 1 atmega 1 vscode-snippets 1 binders 1 ai2001-dataset 1 ai2001-development 1 dataset 1 isabelle-lang 1 isabelle-sc-dataset 1 r-language 1 rmarkdown-language 1 source-code-dataset 1 isar 1 big-data 1 randomized-algorithms 1 cvc4 1 higher-order 1 model-finding 1 sat 1 lambda 1 ethereum 1 smart-contracts 1 dependent-type-theory 1 web-ide 1 algorithms 1 algorithms-datastructures 1 algoritmica 1 estructuras-de-datos 1 funcional-programming 1 programacion-funcional 1 probability 1 pluto 1 exercises 1 se 1 geometry 1 inference 1 optimization 1 reasoning 1 abstract-algebra 1 docker-image 1 texlive 1 vagrant 1 virtual-machine 1 vm 1 dependent-types 1 logical-framework 1 counterexamples 1 quickcheck 1 emacs 1 model-checker 1 timed-automata 1 coc-extension 1 ide 1 isaebelle-lang 1 programming 1 snu 1 snu-2d 1 snu-2d-programming-tools 1 snu-2d-programmingtools 1