Ecosyste.ms: Repos

An open API service providing repository metadata for many open source software ecosystems.

GitHub topics: isabelle-hol

Repositories

au-ts/cogent

Cogent Project

Language: Isabelle - Size: 17.2 MB - Last synced: 5 days ago - Pushed: over 1 year ago - Stars: 157 - Forks: 26

awesomo4000/awesome-provable

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

Size: 25.4 KB - Last synced: 7 days ago - Pushed: over 2 years ago - Stars: 187 - Forks: 8

jaalonso/Lecturas_GLC

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

Size: 5.73 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 62 - Forks: 8

lukaskollmer/advent-of-code

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

Language: OCaml - Size: 269 KB - Last synced: about 2 months ago - Pushed: 5 months ago - Stars: 1 - Forks: 0

Kuniwak/isabelle-program-semantics-exercise

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

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

marco10507/formalization-of-sorting-algorithms

some sorting algorithms' formalisation

Language: Isabelle - Size: 665 KB - Last synced: 3 months ago - Pushed: almost 5 years ago - Stars: 5 - Forks: 0

appgvs/fv-project

Formally Verified Conflict-Free Replicated Data Types

Language: Isabelle - Size: 77.1 KB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 1 - Forks: 0

atakeskinn/eudoxus-reals

An unusual construction of the real numbers using Isabelle/HOL

Language: Isabelle - Size: 814 KB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 0 - Forks: 0

atakeskinn/martingales

A Formalization of Martingales using Isabelle/HOL

Language: Isabelle - Size: 20 MB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 0 - Forks: 0

diekmann/kant

Kategorischer Imperativ in Isabelle/HOL (experimental)

Language: Isabelle - Size: 8.95 MB - Last synced: 8 months ago - Pushed: 8 months ago - Stars: 3 - Forks: 0

qin-yu/concurrent-separation-logic-soundness

2017 [Isabelle2016-1] soundness proof for concurrent separation logic (CSL)

Language: Isabelle - Size: 548 KB - Last synced: 8 months ago - Pushed: over 5 years ago - Stars: 0 - 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: 9 months ago - Pushed: 9 months 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: 9 months ago - Pushed: over 4 years ago - Stars: 0 - Forks: 0

carlinmack/afp

Language: HTML - Size: 247 MB - Last synced: 10 months ago - Pushed: almost 2 years ago - Stars: 1 - Forks: 0

pefribeiro/isabelle-hol-texlive

Isabelle-HOL with TeXlive docker image

Language: Dockerfile - Size: 5.86 KB - Last synced: 10 months ago - Pushed: about 5 years ago - Stars: 0 - Forks: 0

dominique-unruh/bounded-operators

Isabelle theory about bounded operators

Language: Isabelle - Size: 11.9 MB - Last synced: 10 months ago - Pushed: over 2 years ago - Stars: 2 - Forks: 1

Davetbutler/formalising-mpc-isabelle

Formalisation of MPC in Isabelle/HOL

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

logicalhacking/Featherweight_OCL

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

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

sorenmulli/draw-isabelle

Viz Isabelle ⟨l, a, r⟩ graphs

Language: Python - Size: 4.88 KB - Last synced: about 2 months ago - Pushed: about 1 year ago - Stars: 0 - Forks: 0

DavidSanan/davidsanan.github.io

Language: CSS - Size: 7.41 MB - Last synced: 11 months ago - Pushed: about 1 year 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: about 1 year ago - Pushed: almost 4 years ago - Stars: 1 - Forks: 0

adbrucker/isabelle-hacks

A Collection of Isabelle Programming Hacks

Language: Standard ML - Size: 393 KB - Last synced: about 1 year ago - Pushed: about 1 year ago - Stars: 2 - Forks: 1

aureleeNet/formalizations

This repository collects project-relevant Isabelle/HOL formalizations.

Language: Isabelle - Size: 102 KB - Last synced: about 1 year ago - Pushed: over 2 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: about 1 year ago - Pushed: over 2 years ago - Stars: 2 - Forks: 0

jaalonso/RA20116

Curso de "Razonamiento automático"

Language: Isabelle - Size: 35.2 KB - Last synced: about 1 year ago - Pushed: almost 2 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: about 1 year ago - Pushed: almost 2 years ago - Stars: 1 - Forks: 0

jaalonso/AFV

Algorítmica funcional verificada

Language: Isabelle - Size: 81.1 KB - Last synced: about 1 year ago - Pushed: almost 2 years ago - Stars: 0 - Forks: 0

jaalonso/Cursos_de_RA

Recopilación de cursos de razonamiento automático.

Size: 15.6 KB - Last synced: about 1 year ago - Pushed: almost 2 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: about 1 year ago - Pushed: almost 2 years ago - Stars: 0 - Forks: 0

Related Keywords

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