Git Product home page Git Product logo

  • CoqHammer: An automated reasoning hammer tool for Coq - proof automation for dependent type theory.

  • Coinduction: A Coq plugin to help with proofs by coinduction.

  • HCPL: A prototypical proof checker and programming language based on illative combinatory logic.

  • Javalette: An educational compiler for Javalette, written in C.

  • CMakefile: Automatic build system for C and C++.

  • COQ-IMP: Coq version of (part of) the HOL-IMP theories accompanying the book "Concrete Semantics with Isabelle/HOL".

  • CLC: Confluence of an Extension of Combinatory Logic by Boolean Constants: a formalisation of the solution to the RTA open problem 15.

  • infinitary-confluence: Formalisation of a coinductive confluence proof for the infinitary lambda calculus.

  • sortalgs: Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.

  • BST: Binary Search Trees in Coq.

  • Diaconescu: Formalisation of two variants of Diaconescu's theorem.

  • tptp2coq: Conversion of the FOF TPTP format to Coq files.

  • tptp2ileancop: Run ileancop on the ILTP library.

Łukasz Czajka's Projects

asm32 icon asm32

An educational assembler for a subset of 32bit x86 instructions.

bst icon bst

Binary Search Trees in Coq

cfoprover icon cfoprover

An experimental connection-driven prover for intuitionistic first-order logic

clc icon clc

Confluence of an Extension of Combinatory Logic by Boolean Constants: a formalisation of the solution to the RTA open problem 15.

coq icon coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

coq-imp icon coq-imp

Coq version of (part of) the HOL-IMP theories accompanying the book "Concrete Semantics with Isabelle/HOL". Formalized using a now outdated version of CoqHammer.

coqhammer icon coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

diaconescu icon diaconescu

Formalisation of two variants of Diaconescu's theorem

dict2 icon dict2

A dictionary viewing application for Linux.

hcpl icon hcpl

A prototypical proof checker and programming language based on illative combinatory logic

hexcalc icon hexcalc

A calculator which lets you see the results of various x86 instructions. Written in x86 assembly.

javalette icon javalette

An educational compiler for Javalette, written in C

mcp icon mcp

A simple macro processor.

minijuvix icon minijuvix

A functional language for writing validity predicates

opam-coq-archive icon opam-coq-archive

Archive for all Coq related OPAM packages organized in various repositories

pascaladt icon pascaladt

A library of algorithms and data structures for the Free Pascal Compiler.

ramsey icon ramsey

Proof of the finite Ramsey's theorem.

smtcoq icon smtcoq

Communication between Coq and SAT/SMT solvers

snake icon snake

A snake game for Linux written in x86 assembly.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.