Łukasz Czajka (@lukaszcz)
github

lukaszcz

Twitter logo Share LinkedIn logo Share Facebook logo Share
  • Stars
    star
    233
  • Global Rank 109,269 (Top 4 %)
  • Registered over 15 years ago
  • Most used languages
    Coq     36.4 %
    C
         18.2 %
    OCaml
         18.2 %
    Haskell
         18.2 %
    Pascal     9.1 %

Top repositories

1

coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
OCaml
210
star
2

infinitary-confluence

Formalisation of a coinductive confluence proof for the infinitary lambda calculus.
Coq
8
star
3

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.
Coq
6
star
4

coinduction

A Coq plugin to help with proofs by coinduction.
OCaml
6
star
5

tptp2coq

Conversion of the FOF TPTP format to Coq files
Haskell
4
star
6

javalette

An educational compiler for Javalette, written in C
C
2
star
7

asm32

An educational assembler for a subset of 32bit x86 instructions.
C
1
star
8

pascaladt

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

sortalgs

Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.
Coq
1
star
10

clc

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

cfoprover

An experimental connection-driven prover for intuitionistic first-order logic
Haskell
1
star