Topic: "proofs"
nayuki/Project-Euler-solutions
Runnable code for solving Project Euler problems in Java, Python, Mathematica, Haskell.
Language: Java - Size: 2.52 MB - Last synced at: 11 days ago - Pushed at: 11 months ago - Stars: 1,924 - Forks: 677
FStarLang/karamel
KaRaMeL is a tool for extracting low-level F* programs to readable C code
Language: OCaml - Size: 12.3 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 441 - Forks: 65
hoytech/quadrable
Authenticated multi-version database: sparse binary merkle tree with compact partial-tree proofs
Language: C++ - Size: 442 KB - Last synced at: 17 days ago - Pushed at: about 2 years ago - Stars: 302 - Forks: 15
AeneasVerif/aeneas
A verification toolchain for Rust programs
Language: OCaml - Size: 8.35 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 253 - Forks: 24
spamegg1/Math-for-CS-solutions
Solutions to In-Class questions, Problem Sets and Exams of MIT Mathematics for Computer Science 2015 (same as 2019 Open Learning Library)
Language: TeX - Size: 11.5 MB - Last synced at: about 1 month ago - Pushed at: 8 months ago - Stars: 150 - Forks: 24
gapt/gapt
GAPT: General Architecture for Proof Theory
Language: Scala - Size: 182 MB - Last synced at: 4 days ago - Pushed at: 16 days ago - Stars: 98 - Forks: 18
spamegg1/Epp-Discrete-Math-5th-solutions
Solutions to Susanna Epp's Discrete Mathematics book, 5th Edition
Language: TeX - Size: 67.2 MB - Last synced at: about 1 month ago - Pushed at: about 2 months ago - Stars: 97 - Forks: 23
ZKProofs/ZKProofs.github.io
ZKProofs website
Size: 163 KB - Last synced at: 13 days ago - Pushed at: over 1 year ago - Stars: 89 - Forks: 52
wiktor-k/openpgp-proofs
Like Keybase but distributed
Language: JavaScript - Size: 43 KB - Last synced at: 7 months ago - Pushed at: over 1 year ago - Stars: 54 - Forks: 4
miguelmota/zksnarks-example 📦
An example of how generate zero-knowledge proofs and verify using an Ethereum smart contract.
Size: 22.5 KB - Last synced at: about 1 year ago - Pushed at: over 5 years ago - Stars: 35 - Forks: 8
philzook58/lens-algebra
Type level algebraic "proofs" using lens combinators
Language: Haskell - Size: 20.5 KB - Last synced at: 22 days ago - Pushed at: over 5 years ago - Stars: 19 - Forks: 0
chakravala/Math-Research-Notes
Theorems, Definitions, Papers, Research
Language: TeX - Size: 1.38 MB - Last synced at: 17 days ago - Pushed at: almost 6 years ago - Stars: 17 - Forks: 4
sapienzastudentsnetwork/basi-di-dati-1
[Informatica - Basi di Dati 1] Forum di scambio e confronto di soluzioni a esercizi e prove d'esame passate
Size: 40 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 16 - Forks: 0
KiJeong-Lim/portfolio
My portfolio contains a lexer generator, a parser generator, my own λProlog interpreter, and several meta-theorems for the propositional logic with their proofs written in Coq.
Size: 1.58 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 14 - Forks: 0
evdenis/acsl-proved
Fully proved small C functions (examples for verification course).
Language: C - Size: 598 KB - Last synced at: about 1 year ago - Pushed at: almost 8 years ago - Stars: 14 - Forks: 0
sstucki/f-omega-int-agda
F-omega with interval kinds mechanized in Agda
Language: Agda - Size: 448 KB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 13 - Forks: 3
VariantSync/Vatras
Agda Library to Study the Expressive Power of Languages for Static Variability
Language: Agda - Size: 1.51 MB - Last synced at: about 1 hour ago - Pushed at: 4 days ago - Stars: 12 - Forks: 0
marnix/zigmmverify
Language: Zig - Size: 250 KB - Last synced at: about 2 years ago - Pushed at: about 3 years ago - Stars: 10 - Forks: 0
nyu-acsys/template-proofs
Template-based proofs of concurrent search structures.
Language: Coq - Size: 2.37 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 9 - Forks: 2
ph4r05/masterThesis
My master thesis on Whitebox cryptography & AES Whitebox schemes.
Language: TeX - Size: 8.11 MB - Last synced at: 20 days ago - Pushed at: almost 11 years ago - Stars: 9 - Forks: 3
acorrenson/Oratio
Translate natural deduction proofs into natural language.
Language: OCaml - Size: 11 MB - Last synced at: 21 days ago - Pushed at: about 4 years ago - Stars: 8 - Forks: 1
Lolirofle/stuff-in-agda
Formal proofs in mathematics/computer science/logic formalized in the Agda language. A hobby project I am working on in my free time.
Language: Agda - Size: 4.67 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 7 - Forks: 1
jsign/go-unixfs-proof
UnixFS DAG files offset-based proofs
Language: Go - Size: 240 KB - Last synced at: 24 days ago - Pushed at: about 2 years ago - Stars: 6 - Forks: 1
hazelgrove/hazelnut-livelits-agda
mechanization for livelits paper, https://github.com/hazelgrove/livelits-paper
Language: Agda - Size: 585 KB - Last synced at: about 2 months ago - Pushed at: about 4 years ago - Stars: 6 - Forks: 0
signchain/core
Digital signing tool for legal contracts
Language: JavaScript - Size: 107 MB - Last synced at: about 2 years ago - Pushed at: about 4 years ago - Stars: 6 - Forks: 3
danilkolikov/setoids
Idris proofs for extensional equalities
Language: Idris - Size: 14.6 KB - Last synced at: almost 2 years ago - Pushed at: almost 7 years ago - Stars: 6 - Forks: 1
keithstellyes/csproofs
Just some of my CS Proofs, things like why `k << 1 == k * 2`
Language: TeX - Size: 390 KB - Last synced at: over 1 year ago - Pushed at: about 8 years ago - Stars: 6 - Forks: 2
binary-translation/risotto-proofs
Proofs for the paper "Risotto: A Dynamic Binary Translator for Weak Memory Model Architectures"
Language: Agda - Size: 138 KB - Last synced at: 7 days ago - Pushed at: over 2 years ago - Stars: 5 - Forks: 0
Yash-Bhange/Blockchain-based-Self-Concious-House
A self-conscious house (digital twin) that manages all your house related bills and home improvements which is capable of monitoring government issued subsidies and apply for them when the house its action framework matches the subsidy. This way, we unburden the house owner of house-related management tasks or the need for being aware of each government issued subsidy. Only recognized contractors are able to join the reversed marketplace where they can bid for house related jobs like installing solar panels. The house will suggest the most fitting contractor, however, the final decision lies with the house owner. The government benefits from this system as it can monitor the progress of its subsidies and tailor it if needed. It's a more efficient way of spreading information with regards to subsidies.
Language: JavaScript - Size: 7.15 MB - Last synced at: about 1 year ago - Pushed at: over 4 years ago - Stars: 5 - Forks: 1
v--/notebook
Personal notes of various topics in mathematics
Language: TeX - Size: 9.84 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 4 - Forks: 0
EuroProofNet/ATP
Repository of EuroProofNet WG 2 on ATPs
Language: OpenEdge ABL - Size: 28.3 KB - Last synced at: 3 months ago - Pushed at: almost 2 years ago - Stars: 4 - Forks: 1
michpara/CSI2120-Programming-Paradigms
Labs for Programming Paradigms
Language: HTML - Size: 38.1 KB - Last synced at: 11 days ago - Pushed at: almost 4 years ago - Stars: 4 - Forks: 1
aartifact/aartifact-verifier
Lightweight formal verification system developed to support research on usability of automated proof verification tools.
Language: Haskell - Size: 194 KB - Last synced at: about 1 year ago - Pushed at: over 7 years ago - Stars: 4 - Forks: 0
cuppajoeman/openmath
Language: HTML - Size: 2.99 MB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 3 - Forks: 6
craigmateo/courses
Code and files from coursework, tutorials, moocs, etc.
Language: HTML - Size: 106 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 3 - Forks: 0
metamath/lamp-guide
Guide on how to use the metamath-lamp proof assistant
Language: HTML - Size: 22.2 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 3 - Forks: 1
Gyakobo/Recognizing-context-free-languages-with-a-PDA
The following project should define a PDA that in its turn would recognize a specific context-free language.
Language: Python - Size: 107 KB - Last synced at: about 2 months ago - Pushed at: 11 months ago - Stars: 3 - Forks: 0
zchn/eth-acl2
An ACL2 formalization of the Ethereum VM, aiming to be both executable and suitable for proving interesting properties of EVM contracts.
Language: Common Lisp - Size: 249 KB - Last synced at: 5 months ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 3
gz101/mit6042j
Self study of selected parts of MIT's 6.042j Mathematics for Computer Science as recommended in Harvard's CS121 Introduction to Theoretical Computer Science preparation.
Size: 767 KB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 0
yurrriq/friendly-intro-to-group-theory
Working through the exercises in "A Friendly Introduction to Group Theory"
Language: Nix - Size: 354 KB - Last synced at: about 2 months ago - Pushed at: over 4 years ago - Stars: 3 - Forks: 0
jcagarcia/proofs
Repository to upload my own proofs of concept and some code examples
Language: AspectJ - Size: 23.1 MB - Last synced at: 22 days ago - Pushed at: almost 7 years ago - Stars: 3 - Forks: 3
Mari-W/System-Fo
formal proof of type preservation of the dictionary passing transform for system f
Language: Agda - Size: 13.1 MB - Last synced at: about 1 year ago - Pushed at: about 2 years ago - Stars: 2 - Forks: 0
YufeiCui/CSCB63
Design and Analysis of Data Structures
Size: 392 KB - Last synced at: about 2 years ago - Pushed at: about 6 years ago - Stars: 2 - Forks: 0
dragonwasrobot/formal-moessner
A formal study of Moessner's sieve
Language: Coq - Size: 1.51 MB - Last synced at: about 1 month ago - Pushed at: about 6 years ago - Stars: 2 - Forks: 0
chenxingqiang/zero-knowledge-proofs
Zero Knowledge Proofs focusing on Basic Concepts, Interactive Learning, Zero Knowledge Proof Systems Comparison, Courses and Tutorials, SNARKs.
Size: 916 KB - Last synced at: about 1 month ago - Pushed at: 5 months ago - Stars: 1 - Forks: 0
spamegg1/spamegg1-lean
Working through Functional Programming in Lean
Language: Lean - Size: 50.8 KB - Last synced at: about 1 month ago - Pushed at: 6 months ago - Stars: 1 - Forks: 0
trustops/awesome-trustops
A list of tools and methods for building trustworthy software following TrustOps principles.
Size: 750 KB - Last synced at: 7 months ago - Pushed at: 8 months ago - Stars: 1 - Forks: 0
Gyakobo/Recognizing-an-email-adress-with-DFA
The following example is meant to demonstrate how a Deterministic Finite Automata(DFA) algorithm is supposed to guide identify whether a string is an email adress ending with .gov or .gr
Language: Python - Size: 134 KB - Last synced at: 5 months ago - Pushed at: 10 months ago - Stars: 1 - Forks: 0
PriorLax123/Propositional_Logic
This Project shows an understanding of Propositional Logic, Conjunctive Normal Form, and The Resolution Refutation Method.
Language: Java - Size: 18.6 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0
luqmanmalik/Analysis-MathML
Requirements: Safari Webkit 17.1 (⥣) | Analysis in MathML© Foundations in Mathematical Analysis | Watters Research and Technologies® | MIT License | BSD (C4)-License | Analogue: UCB Math 104: Introductory Analysis
Language: HTML - Size: 5.48 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0
gvsuoer/sundstrom-textbook
Language: TeX - Size: 121 MB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 2
Hosein-Rahnama/Mathematical-Theorems
This is a collection of proofs for some mathematical theorems.
Language: TeX - Size: 271 KB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0
benjaminkiesl/drat2er
drat2er: Proof Transformer for Propositional Logic
Language: C++ - Size: 906 KB - Last synced at: about 2 years ago - Pushed at: over 3 years ago - Stars: 1 - Forks: 2
Mandarancio/ProofKit
ADT and Proof editor
Language: Swift - Size: 917 KB - Last synced at: 7 days ago - Pushed at: over 3 years ago - Stars: 1 - Forks: 1
skykanin/Proofs
Collection of formal proofs
Language: Idris - Size: 62.5 KB - Last synced at: about 1 year ago - Pushed at: almost 4 years ago - Stars: 1 - Forks: 0
akayibrahim/challenge
Social Network For Competition - Project 3
Language: Java - Size: 1.59 MB - Last synced at: 2 months ago - Pushed at: about 4 years ago - Stars: 1 - Forks: 0
rubenseyer/pistophylax
Natural deduction proof assistant
Language: Python - Size: 60.5 KB - Last synced at: 22 days ago - Pushed at: over 4 years ago - Stars: 1 - Forks: 0
logic-proof-checker/capstone-openLogic
Capstone Spring 2019
Language: JavaScript - Size: 1.44 MB - Last synced at: about 2 years ago - Pushed at: almost 6 years ago - Stars: 1 - Forks: 6
minhnhdo/programming-language-foundations-in-idris
Programming language foundations in Idris
Language: Idris - Size: 145 KB - Last synced at: about 2 years ago - Pushed at: almost 6 years ago - Stars: 1 - Forks: 0
mattdean1/functional-programming
Exercises in Agda
Language: Agda - Size: 63.5 KB - Last synced at: about 2 months ago - Pushed at: over 6 years ago - Stars: 1 - Forks: 0
ZcashJS/zcash-redux 📦
Zcash Redux - Redux helper for connecting to Zcash Daemon
Language: JavaScript - Size: 106 KB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 1 - Forks: 0
joda2802/Proofs
Language: TeX - Size: 187 KB - Last synced at: about 2 years ago - Pushed at: about 7 years ago - Stars: 1 - Forks: 0
vincentlaucsb/UCSB-MATH-122AB--Complex-Variables
A collection of notes, summary sheets, and homework for UCSB's complex analysis series.
Language: TeX - Size: 5.52 MB - Last synced at: 2 months ago - Pushed at: over 7 years ago - Stars: 1 - Forks: 1
EduPH/Teoria-Matematica
RecolecciĂłn de teorĂa, teoremas y demostraciones
Language: TeX - Size: 1.78 MB - Last synced at: about 2 years ago - Pushed at: over 7 years ago - Stars: 1 - Forks: 0
eadm/rational-setoid
Setoid for rational numbers written in Idris
Language: Idris - Size: 12.7 KB - Last synced at: 19 days ago - Pushed at: almost 8 years ago - Stars: 1 - Forks: 0
brendanzab/agda-logic-playground
Messing around with propositional logic in Agda
Language: Agda - Size: 1.95 KB - Last synced at: about 1 month ago - Pushed at: over 8 years ago - Stars: 1 - Forks: 0
eclipse-xfsc/portal-proof-management-service
Manages proofs and proof handlings
Language: TypeScript - Size: 0 Bytes - Last synced at: about 15 hours ago - Pushed at: about 16 hours ago - Stars: 0 - Forks: 0
COSC3020/isomorphism-connectivity
Size: 1.95 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0
COSC3020/little-o
Size: 0 Bytes - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0
COSC3020/isomorphism-nodes-connectivity
Size: 1000 Bytes - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0
COSC3020/isomorphism-nodes
Size: 1000 Bytes - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0
filemon-mateus/tex-hw
Base LaTeX template useful for formatting homework assignments.
Language: TeX - Size: 465 KB - Last synced at: 2 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0
kavishkagihan/AL_Notes
This repository contains a detailed and organized set of notes that I've put together throughout my AL studies. These notes cover key concepts, formulas, practical and principles in each subject, serving as a useful resource for revision or self-study.
Size: 838 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0
cybers1t/koans.lean
Lean4 Zen Koans. Each file implements an algorithm. Several files may come together to form a programming language.
Language: Lean - Size: 8.79 KB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 0 - Forks: 0
rnibhriain/functional-programming
Functional programming :desktop_computer: Haskell assignments for Functional Programming module: CSU34016
Language: Haskell - Size: 2.83 MB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 0 - Forks: 0
domschrei/impcheck
Immediate Massively Parallel Propositional Proof Checking
Language: C - Size: 93.8 KB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 0 - Forks: 0
kristomu/voting-scripts
Miscellaneous voting method scripts
Language: Python - Size: 66.4 KB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 0 - Forks: 0
jackr276/Email-Address-Recognition-with-a-DFA
Implementation of a Deterministic Finite Automaton for email address recognition
Language: C++ - Size: 188 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0
SavouryGin/chop_logic_poc
Pet project for developing a React interface, which will allow to construct logical proofs and calculate other logical stuff.
Language: TypeScript - Size: 3.12 MB - Last synced at: 30 days ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
sourcedennis/agda-dodo
Binary relations library written in Agda
Language: Agda - Size: 46.9 KB - Last synced at: 7 days ago - Pushed at: about 2 years ago - Stars: 0 - Forks: 0
UofSC-Spring-2023-SCHC-411-H01/homework03
Predicate logic through relations in Lean
Language: Lean - Size: 5.86 KB - Last synced at: over 1 year ago - Pushed at: about 2 years ago - Stars: 0 - Forks: 0
lukegeel101/Writing-in-Mathematics
MATH370 Taught by Andrew Havens at UMass Amherst Spring 2022
Language: TeX - Size: 1.91 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
UofSC-Fall-2022-Math-300-H01/homework10
Proving properties of functions on paper and in Lean
Language: Lean - Size: 104 KB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
asubramanian08/PACT-Group-2
Approximation and randomized algorithms - PACT group 2 with Dr. Rajiv Gandhi
Size: 19.5 KB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
Daniyal-Murtaza/Discrete-maths-tex-solutions
This repo consists of the solutions of discrete mathematics' homework. It was obliged to be done in the latex format.
Language: TeX - Size: 25.4 KB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
asubramanian08/PACT-Group-1
Theoretical Computer Science - PACT group 1 with Dr. Rajiv Gandhi
Size: 5.99 MB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0
chrisjpm/holbert Fork of liamoc/holbert
A graphical interactive proof assistant designed for education. My contributions: applying rules by elimination, proofs by induction, proofs by cases, multi-axiom element and misc css styling. Honours report grade: 76% :tada:
Language: Haskell - Size: 13.3 MB - Last synced at: over 1 year ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0
UT1/Project-Euler
Solutions to problems on projecteuler.net
Language: Java - Size: 121 KB - Last synced at: about 2 years ago - Pushed at: about 3 years ago - Stars: 0 - Forks: 0
cluesurfback/math
Math in XO
Size: 22.5 KB - Last synced at: 21 days ago - Pushed at: almost 4 years ago - Stars: 0 - Forks: 0
stoand/kakoune-arend
Unofficial syntax highlighting for the Arend Language for the Kakoune editor
Size: 3.91 KB - Last synced at: about 1 year ago - Pushed at: over 4 years ago - Stars: 0 - Forks: 0
JohnItoo/StPetersbug-Core-Skills
This is a walkthrough of my solutions to exercises in CP-Core-Skills course offered by StPetersburg University, Russia.
Language: Java - Size: 41 KB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 0 - Forks: 0
severen/maths
Notes on mathematics at an undergraduate level.
Language: TeX - Size: 996 KB - Last synced at: about 2 months ago - Pushed at: almost 5 years ago - Stars: 0 - Forks: 0
alvarofpp/course-coq 📦
ExercĂcios do curso de introdução ao Coq criado por Rodrigo Ribeiro
Language: Coq - Size: 14.6 KB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 0 - Forks: 0
ajayeeralla/real-or-random-auth-proofs-coq
Machine-checked proofs of secrecy and authentication using CCSA framework
Language: Coq - Size: 2.37 MB - Last synced at: about 2 years ago - Pushed at: about 5 years ago - Stars: 0 - Forks: 0
bharathkarumudi/Certified-Security-By-Design
Certified-Security-By-Design
Language: Standard ML - Size: 6.71 MB - Last synced at: 5 days ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0
minhnhdo/programming-language-foundations-in-lean
Programming language foundations in Lean
Language: Lean - Size: 118 KB - Last synced at: about 2 years ago - Pushed at: almost 6 years ago - Stars: 0 - Forks: 0
pavponn/math-logic
Homework from Mathematical Logic 2019 course in ITMO University.
Language: Haskell - Size: 92.8 KB - Last synced at: about 2 years ago - Pushed at: about 6 years ago - Stars: 0 - Forks: 0
yisus82/fic-md2
Matemática Discreta - Facultad de Informática de A Coruña
Language: Coq - Size: 29.3 KB - Last synced at: about 1 month ago - Pushed at: about 6 years ago - Stars: 0 - Forks: 0
kkulewski/logic
Logic in Computer Science 2018/2019
Language: Objective-J - Size: 13.7 KB - Last synced at: about 2 years ago - Pushed at: about 6 years ago - Stars: 0 - Forks: 0
KokorinIlya/math_logic
Homeworks for math logic course in ITMO University
Language: Java - Size: 3.91 MB - Last synced at: 23 days ago - Pushed at: almost 7 years ago - Stars: 0 - Forks: 0
