isabelle-hol

Here are 38 public repositories matching this topic...

au-ts / cogent

Star 140

Cogent Project

verification programming-languages file-systems isabelle-hol co-generation

• Updated Jul 21, 2021
• Isabelle

awesomo4000 / awesome-provable

Star 124

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

coq idris agda isabelle formal-verification isabelle-hol sel4 certified-programming

• Updated Jul 23, 2019

jaalonso / Lecturas_GLC

Star 27

Lecturas del Grupo de Lógica Computacional

haskell functional-programming coq logic prolog logic-programming isabelle-hol itp leanprover

• Updated Jul 31, 2021

josephcmac / Folklore-and-miscellaneous-results-in-number-theory

Star 9

Formal verification of folklore and miscellaneous results in number theory

formal-verification number-theory isabelle-hol

• Updated Feb 2, 2020
• Isabelle

marco10507 / formalization-of-sorting-algorithms

Star 4

some sorting algorithms' formalisation

mergesort insertion-sort selection formalization isabelle-hol

• Updated Aug 17, 2019
• Isabelle

diekmann / Isabelle-Hello-World

Star 3

Hello World in Isabelle, compiled to Haskell

haskell functional-programming isabelle-hol

• Updated Mar 7, 2020
• Isabelle

jaalonso / RA20116

Star 2

Curso de "Razonamiento automático"

isabelle isabelle-hol

• Updated Nov 25, 2016
• Isabelle

jaalonso / SLP

Star 1

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

isabelle isabelle-hol

• Updated Jul 26, 2017
• Isabelle

Davetbutler / formalising-mpc-isabelle

Star 1

Formalisation of MPC in Isabelle/HOL

cryptography formal-methods formal-verification isabelle-hol multi-party-computation

• Updated Mar 2, 2021
• Isabelle

pilif0 / bigraph

Star 1

Formalization of Robin Milner's bigraphs in Isabelle/HOL

formalization isabelle-hol

• Updated Aug 21, 2019
• Isabelle

SvenWille / LogicForwardProofs

Star 1

Propositional logic and FOL proofs (froward style)

logic exercise isabelle propositional-logic isabelle-hol natural-deduction fol fitch-proofs

• Updated Dec 2, 2017
• Isabelle

carlinmack / afp

Star 1

isabelle isabelle-hol

• Updated Jul 29, 2021
• HTML

AnthonyBordg / Isabelle_marries_Desargues

Star 1

A formalization of projective geometry in Isabelle

isabelle-hol projective-geometry

• Updated Jun 26, 2019
• Isabelle

logicalhacking / Featherweight_OCL

Star 1

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

firewall verification ocl isabelle-hol hol formal-proofs holocl

• Updated Mar 11, 2021
• Isabelle

celinadongye / Isabelle-exercises

Star 1

logic first-order-logic propositional-logic isabelle-hol

• Updated Nov 17, 2019
• Isabelle

celinadongye / Geometry-of-Sections

Star 1

Theorem proving geometry of sections in Isabelle

geometry optimization logic inference isabelle isabelle-hol reasoning

• Updated Dec 20, 2019
• Isabelle

dominique-unruh / bounded-operators

Star 1

Isabelle theory about bounded operators

isabelle-hol

• Updated Jul 15, 2021
• Isabelle

ZenutkinN / university.labs.formal-software-verification

Star 0

Laboratory work on the university course "Formal software verification"

bash university labs promela haskel spin isabelle-hol

• Updated Dec 29, 2020
• C

SatyendraBanjare / ATP-proofs

Star 0

Collection of explainatory example proofs for popular proof assistants.

proof-of-concept coq proof-assistant type-theory isabelle-hol homotopy-type-theory typesystems

• Updated Aug 21, 2018
• Coq

pefribeiro / isabelle-hol-texlive

Star 0

Isabelle-HOL with TeXlive docker image

docker-image texlive isabelle isabelle-hol

• Updated Apr 15, 2019
• Dockerfile

rizaldialbert / vhdl-semantics

Star 0

proof proof-assistant formal-methods isabelle formal-verification isabelle-hol itp interactive-theorem-proving formal-proofs

• Updated Dec 7, 2020
• Isabelle

jaalonso / AFV

Star 0

Algorítmica funcional verificada

algorithms isabelle isabelle-hol algorithms-datastructures estructuras-de-datos funcional-programming algoritmica programacion-funcional

• Updated Feb 25, 2019
• Isabelle

m0t0k1ch1 / prog-prove

Star 0

Programming and Proving in Isabelle/HOL

isabelle isabelle-hol

• Updated Jul 11, 2018
• Isabelle

logicalhacking / Automated_Stateful_Protocol_Verification

Star 0

Local mirror of Stateful Protocol Composition and Typing entry of the Archive of Formal Proofs (AFP).

verification isabelle-hol protocol-verification security-protocols

• Updated Mar 11, 2021
• Isabelle

logicalhacking / UPF

Star 0

Local mirror of The Unified Policy Framework (UPF) entry of the Archive of Formal Proofs (AFP).

access-control isabelle-hol afp policy-framework

• Updated Mar 11, 2021
• Isabelle

jaalonso / TFG_de_Carlos

Star 0

Elementos de matemáticas formalizados en Isabelle/HOL

mathematics isabelle-hol

• Updated Jun 17, 2020
• Isabelle

logicalhacking / UPF_Firewall

Star 0

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

firewall iptables isabelle-hol afp

• Updated Mar 11, 2021
• Isabelle

logicalhacking / Stateful_Protocol_Composition_and_Typing

Star 0

verification isabelle-hol protocol-verification security-protocols

• Updated Mar 11, 2021
• Isabelle

jaalonso / Cursos_de_RA

Star 0

Recopilación de cursos de razonamiento automático.

coq proof-assistant courses agda lean isabelle-hol prover9 pvs interactive-theorem-proving otter automated-reasoning acl2

• Updated Feb 1, 2020

helli / tsp-approximation

Star 0

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

isabelle-hol tsp-approximation

• Updated Oct 16, 2019
• Isabelle

Load more…