GitHub topics: isabelle-hol

Repositories

jaalonso/Lecturas_GLC

Readings on computational logic, interactive theorem proving and functional programming.

Size: 6.97 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 75 - Forks: 8

awslabs/AutoCorrode

Verification infrastructure for the Isabelle/HOL interactive proof assistant

Language: Isabelle - Size: 477 KB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 4 - Forks: 1

au-ts/cogent

Cogent Project

Language: Isabelle - Size: 17.2 MB - Last synced at: 4 days ago - Pushed at: about 1 month ago - Stars: 163 - Forks: 27

jaalonso/Calculemus2

Proof exercises in Lean4 and Isabelle/HOL

Language: Lean - Size: 16.1 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 8 - Forks: 0

DavidSanan/davidsanan.github.io

Language: CSS - Size: 7.41 MB - Last synced at: 15 days ago - Pushed at: 15 days ago - Stars: 0 - Forks: 0

awesomo4000/awesome-provable

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

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

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: 5 months ago - Stars: 2 - Forks: 0

diekmann/kant

Kategorischer Imperativ in Isabelle/HOL (experimental)

Language: Isabelle - Size: 8.95 MB - Last synced at: 24 days ago - Pushed at: over 1 year ago - Stars: 4 - Forks: 0

logicalhacking/Featherweight_OCL

Local mirror of Featherweight OCL entry of the Archive of Formal Proofs (AFP).

Language: Isabelle - Size: 446 KB - Last synced at: about 2 months ago - Pushed at: about 3 years ago - Stars: 4 - Forks: 0

Kuniwak/isabelle-program-semantics-exercise

「情報数学講座（第7巻）プログラム意味論」（著: 横内寛文）の形式的証明

Language: Isabelle - Size: 565 KB - Last synced at: 22 days ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 0

ata-keskin/martingales

A Formalization of Martingales using Isabelle/HOL

Language: Isabelle - Size: 20 MB - Last synced at: 14 days ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

marco10507/formalization-of-sorting-algorithms

some sorting algorithms' formalisation

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

logicalhacking/isabelle-ofmc

Isabelle/OFMC - Linking OFMC and Isabelle/HOL

Language: Standard ML - Size: 149 KB - Last synced at: about 2 months ago - Pushed at: over 4 years ago - Stars: 1 - Forks: 0

appgvs/fv-project

Formally Verified Conflict-Free Replicated Data Types

Language: Isabelle - Size: 77.1 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

ata-keskin/eudoxus-reals

An unusual construction of the real numbers using Isabelle/HOL

Language: Isabelle - Size: 814 KB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

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

VTrelat/Hopcroft_verif

Formal verification in Isabelle(HOL) of Hopcroft's algorithm for minimizing DFAs including runtime analysis

Language: Isabelle - Size: 16.2 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

helli/tsp-approximation

an approximation algorithm for the metric travelling salesperson problem, formulated within the Isabelle Refinement Framework

Language: Isabelle - Size: 1.55 MB - Last synced at: over 1 year ago - Pushed at: over 5 years 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

dominique-unruh/bounded-operators

Isabelle theory about bounded operators

Language: Isabelle - Size: 11.9 MB - Last synced at: over 1 year ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 1

Davetbutler/formalising-mpc-isabelle

Formalisation of MPC in Isabelle/HOL

Language: Isabelle - Size: 55.7 KB - Last synced at: almost 2 years ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 1

logicalhacking/UPF_Firewall

Local mirror of Formal Network Models and Their Application to Firewall Policies (UPF-Firewall) entry of the Archive of Formal Proofs (AFP).

Language: Isabelle - Size: 175 KB - Last synced at: about 2 months ago - Pushed at: about 3 years ago - Stars: 0 - Forks: 0

sorenmulli/draw-isabelle

Viz Isabelle ⟨l, a, r⟩ graphs

Language: Python - Size: 4.88 KB - Last synced at: about 2 months ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0

vishallama/fds_ss20 Fork of nipkow/fds_ss20

Lecture course on verified Functional Data Structures

Size: 5.47 MB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 0

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

aureleeNet/formalizations

This repository collects project-relevant Isabelle/HOL formalizations.

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

diekmann/Isabelle-Hello-World

Hello World in Isabelle, compiled to Haskell

Language: Isabelle - Size: 57.6 KB - Last synced at: 24 days ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 0

jaalonso/RA20116

Curso de "Razonamiento automático"

Language: Isabelle - Size: 35.2 KB - Last synced at: about 1 month ago - Pushed at: almost 3 years ago - Stars: 2 - Forks: 0

jaalonso/SLP

Semánticas de lenguajes de programación formalizadas en Isabelle/HOL

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

jaalonso/AFV

Algorítmica funcional verificada

Language: Isabelle - Size: 81.1 KB - Last synced at: about 1 month ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0

jaalonso/Cursos_de_RA

Recopilación de cursos de razonamiento automático.

Size: 15.6 KB - Last synced at: about 1 month ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0

jaalonso/TFG_de_Carlos Fork of Carnunfer/TFG

Elementos de matemáticas formalizados en Isabelle/HOL

Language: Isabelle - Size: 2.86 MB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0

Related Keywords

isabelle-hol 48 isabelle 13 formal-verification 7 proof-assistant 6 logic 5 verification 5 coq 4 theorem-proving 4 formalization 4 formal-proofs 4 functional-programming 3 formal-methods 3 agda 2 proof 2 firewall 2 security-protocols 2 protocol-verification 2 interactive-theorem-proving 2 number-theory 2 reasoning 2 automated-reasoning 2 afp 2 haskell 2 itp 2 lean 2 otter 1 soundness-proof 1 courses 1 acl2 1 programacion-funcional 1 funcional-programming 1 estructuras-de-datos 1 algoritmica 1 homotopy-type-theory 1 proof-of-concept 1 algorithms-datastructures 1 algorithms 1 type-theory 1 typesystems 1 argumentation-frameworks 1 sml 1 functional-data-structure 1 algorithms-and-data-structures 1 algebra 1 optimization 1 inference 1 ring 1 geometry 1 docker-image 1 minkowski-space 1 projective-geometry 1 pluto 1 texlive 1 policy-framework 1 access-control 1 concurrent-separation-logic 1 csl 1 propositional-logic 1 semantic 1 first-order-logic 1 mathematics 1 pvs 1 prover9 1 ocl 1 holocl 1 hol 1 philosophy 1 document 1 ocaml 1 advent-of-code 1 sel4 1 idris 1 certified-programming 1 formalmethods 1 math 1 lean4 1 exercises 1 programming-languages 1 file-systems 1 co-generation 1 rust 1 proof-automation 1 prolog 1 logic-programming 1 leanprover 1 python 1 iptables 1 multi-party-computation 1 cryptography 1 tsp-approximation 1 hopcroft-algorithm 1 automata-theory 1 theoretical-computer-science 1 fibonacci-sequence 1 fibonacci-numbers 1 real-numbers 1 epfl 1 crdts 1 protocol-security 1 ofmc 1