Topic: "type-theory"
lane-core/kitcat
Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda
Language: Agda - Size: 134 KB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 5 - Forks: 0
wkolowski/Type-Theory-Wishlist
Personal research notes
Language: Coq - Size: 1.13 MB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 5 - Forks: 0
epfl-lara/StainlessFit
Stainless directly built on System FR, with standalone front-end
Language: Scala - Size: 30.3 MB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 5 - Forks: 7
varkor/blog
A small blog about type theory and mathematics
Language: HTML - Size: 3.21 MB - Last synced at: about 1 month ago - Pushed at: about 1 year ago - Stars: 4 - Forks: 3
marcoonroad/ownership-disciplines
My own personal list of ownership policies. :microscope: :books: :question: :thinking: [Work in Progress]
Language: Ruby - Size: 11.7 KB - Last synced at: about 2 years ago - Pushed at: about 3 years ago - Stars: 4 - Forks: 0
RobinKa/typed-ga
TypeScript Geometric Algebra implementations with proper typing. Autogenerated using Python and TFGA.
Language: TypeScript - Size: 837 KB - Last synced at: 6 days ago - Pushed at: over 3 years ago - Stars: 4 - Forks: 0
kutyel/thinking-with-types
⌨️ Solutions to the exercises of "Thinking With Types" in various programming languages!
Language: Haskell - Size: 116 KB - Last synced at: about 1 month ago - Pushed at: over 5 years ago - Stars: 4 - Forks: 1
sacerdot/Minimalist-Type-Theory-In-Lambda-Prolog
An implementation in Lambda-Prolog of the Minimalist Type Theory
Language: Prolog - Size: 9.43 MB - Last synced at: about 1 month ago - Pushed at: over 6 years ago - Stars: 4 - Forks: 3
wonks/type-theory-reading-group
IU Type Theory reading group
Language: HTML - Size: 2.66 MB - Last synced at: about 1 year ago - Pushed at: about 7 years ago - Stars: 4 - Forks: 1
chamini2/angler-lang
The Angler Functional Programming Language
Language: Haskell - Size: 308 KB - Last synced at: 2 months ago - Pushed at: about 9 years ago - Stars: 4 - Forks: 0
tambercore/mud
📦 Natural Language Theorem Prover built on Dependent Type Theory (Agda) and Symbolic NLP (Lambeq).
Language: Rust - Size: 15.3 MB - Last synced at: about 10 hours ago - Pushed at: about 10 hours ago - Stars: 3 - Forks: 0
smimram/cccatt
A type theory for unbiased cartesian closed categories.
Language: OCaml - Size: 319 KB - Last synced at: 14 days ago - Pushed at: about 1 month ago - Stars: 3 - Forks: 0
keilambda/ttfpi-agda
Formalization of the book "Type Theory and Formal Proof: An Introduction" in Agda
Language: Agda - Size: 60.5 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 3 - Forks: 0
yiyunliu/system-f-omega
Strong normalization and parametricity for System Fω in Coq
Language: Coq - Size: 235 KB - Last synced at: about 2 months ago - Pushed at: 8 months ago - Stars: 3 - Forks: 1
aripiprazole/zu
🧪 | Zu Theorem Prover
Language: Rust - Size: 299 KB - Last synced at: 8 days ago - Pushed at: over 1 year ago - Stars: 3 - Forks: 0
acorrenson/kind2coq
A experimental compiler from Kind (Core) to Coq
Language: OCaml - Size: 1.95 KB - Last synced at: about 1 month ago - Pushed at: about 3 years ago - Stars: 3 - Forks: 0
ionathanch/ttzoo
Notes on type theory.
Language: TeX - Size: 10.1 MB - Last synced at: 1 day ago - Pushed at: about 4 years ago - Stars: 3 - Forks: 0
MrChico/Smarter-contract-lang
Language: Idris - Size: 208 KB - Last synced at: about 1 month ago - Pushed at: almost 8 years ago - Stars: 3 - Forks: 0
taktoa/mltt Fork of sconybeare/mltt
Implementation of Martin-Löf Type Theory in Haskell
Language: Haskell - Size: 29.3 KB - Last synced at: about 2 years ago - Pushed at: about 9 years ago - Stars: 3 - Forks: 0
pdferreira/tyes
TyES (Type Experiment System) is a personal project in the area of type systems, aiming to provide a playground to test different type system ideas in a simple way.
Language: Scala - Size: 385 KB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 2 - Forks: 0
wrsturgeon/sigma-types
Types automatically checked for invariants in debug builds only.
Language: Rust - Size: 198 KB - Last synced at: 21 days ago - Pushed at: 3 months ago - Stars: 2 - Forks: 0
LebrancWorkshop/Lebranc-Learn-Functional-Programming
I'm learning a Functional Programming by learning its pure math concepts and apply it on functional language like Haskell, Clojure, Elixir, etc.
Language: JavaScript - Size: 198 KB - Last synced at: 2 days ago - Pushed at: about 1 year ago - Stars: 2 - Forks: 3
Shemplo/Study-courses
All individual tasks, homeworks in courses of Java, C++, Haskell, .... at the University
Language: Java - Size: 62.9 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 4
qdeduction/qbar
the rational proof assistant
Language: Rust - Size: 2.49 MB - Last synced at: 6 days ago - Pushed at: almost 2 years ago - Stars: 2 - Forks: 0
LebrancWorkshop/Learn-Haskell-from-Youtube
Learn Haskell from many great resources on Youtube.
Language: Shell - Size: 1.95 KB - Last synced at: about 2 months ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 0
AlgebraicWolf/idris2-russel
Implementation of Russel paradox in Idris 2
Language: Idris - Size: 20.5 KB - Last synced at: almost 2 years ago - Pushed at: almost 4 years ago - Stars: 2 - Forks: 0
aerabi/lttt-report
Report for "A Basis for Event-Driven Programming" based on Linear Temporal Type Theory
Language: TeX - Size: 5.19 MB - Last synced at: about 2 months ago - Pushed at: almost 4 years ago - Stars: 2 - Forks: 0
nguermond/normalization-by-evaluation
Various implementations of normalization by evaluation.
Language: OCaml - Size: 63.5 KB - Last synced at: about 2 years ago - Pushed at: about 4 years ago - Stars: 2 - Forks: 0
mayconamaro/clc-denotational-agda
Minha monografia II da graduação. Semântica Denotacional para o Lambda Cálculo Computacional em Agda
Language: Agda - Size: 4.88 KB - Last synced at: about 2 years ago - Pushed at: about 4 years ago - Stars: 2 - Forks: 0
TomerAberbach/types-and-programming-languages-exercises
My solutions for the exercises presented in Benjamin C. Pierce's Types and Programming Languages.
Size: 4.88 KB - Last synced at: 3 days ago - Pushed at: over 4 years ago - Stars: 2 - Forks: 0
mbrg/lean-tutorial-reference
A newbie's reference solutions to Lean tutorials
Language: Lean - Size: 16.6 KB - Last synced at: 10 months ago - Pushed at: almost 5 years ago - Stars: 2 - Forks: 0
TOTBWF/agda-partial-setoid
An implementation of partial setiods in agda
Language: Agda - Size: 19.5 KB - Last synced at: 2 months ago - Pushed at: almost 6 years ago - Stars: 2 - Forks: 0
jonaprieto/agda-metis
Metis Prover Reasoning for Propositional Logic in Agda
Language: Agda - Size: 765 KB - Last synced at: about 1 month ago - Pushed at: over 6 years ago - Stars: 2 - Forks: 1
danilkolikov/fnn
Experimental Language for Designing of Neural Networks
Language: Kotlin - Size: 242 KB - Last synced at: about 2 years ago - Pushed at: almost 7 years ago - Stars: 2 - Forks: 0
mstn/graphql
personal notes about graphql
Language: TeX - Size: 79.1 KB - Last synced at: about 2 years ago - Pushed at: almost 7 years ago - Stars: 2 - Forks: 0
Centril/interesting-papers
An add space for people to share interesting papers on PLT
Size: 3.91 KB - Last synced at: about 1 month ago - Pushed at: about 7 years ago - Stars: 2 - Forks: 0
vishallama/programming-in-standard-ml
Code examples from the book 'Programming in Standard ML' (2011) by Bob Harper.
Language: Standard ML - Size: 22.5 KB - Last synced at: 10 months ago - Pushed at: about 8 years ago - Stars: 2 - Forks: 1
TheoWinterhalter/local-comp
WIP Local computation rules in type theory
Language: Coq - Size: 287 KB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 1 - Forks: 0
vladyslav005/Lambda
Interactive type checker for simply typed lambda terms
Language: TypeScript - Size: 1.33 MB - Last synced at: 1 day ago - Pushed at: 2 days ago - Stars: 1 - Forks: 0
AbstractionsLab/satrap-dl
SATRAP-DL (Semi-Automated Threat Reconnaissance and Analysis Powered by Description Logics) aims at the development of a platform for interactive computer-aided analysis of cyber threat intelligence driven by logic-based automated reasoning and inference.
Language: Python - Size: 5.01 MB - Last synced at: 22 days ago - Pushed at: 23 days ago - Stars: 1 - Forks: 0
dot-iris/dot-iris.github.io
GitHub Pages website for https://github.com/Blaisorblade/dot-iris.
Language: HTML - Size: 10.4 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 1 - Forks: 0
yurrriq/blorg
C-c C-e P p >>=
Language: CSS - Size: 1.83 MB - Last synced at: about 1 month ago - Pushed at: 3 months ago - Stars: 1 - Forks: 1
jaycech3n/internal-diagrams
WIP: Reedy fibrant diagrams in models of type theory
Language: Agda - Size: 913 KB - Last synced at: about 2 months ago - Pushed at: 5 months ago - Stars: 1 - Forks: 0
lambduli/reading
My digital notepad about Programming Languages Theory, Type Systems, Logic, and Formal Reasoning.
Size: 122 KB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 1 - Forks: 0
Russoul/Nova
A programming language based on extensional Martin Lof Type Theory
Language: Idris - Size: 377 KB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 1 - Forks: 0
matematiflo/SumsOfSquares
Summing squares in Lean
Language: Lean - Size: 24.2 MB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 1 - Forks: 0
vishallama/martin-lof Fork of michaelt/martin-lof
papers of Per Martin Löf
Language: TeX - Size: 121 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 0
workflowfm/workflowfm-reasoner
A logic-based library for correct-by-construction process modelling and composition.
Language: OCaml - Size: 4.19 MB - Last synced at: 5 months ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0
aripiprazole/zure
🧪 | Zure is the remake of Zu but without rigid and unstable types
Language: Rust - Size: 67.4 KB - Last synced at: 8 days ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 2
MxmUrw/Hata 📦
Formalization of topics in mathematics and computer science
Language: Agda - Size: 1.96 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0
cannor147/itmo-tt
Type Theory course at ITMO University
Language: Java - Size: 198 KB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 0
permui/SystemF1
Implementation of the first-order typed lambda calculus as a CLI proof system.
Language: Rust - Size: 118 KB - Last synced at: about 2 years ago - Pushed at: over 3 years ago - Stars: 1 - Forks: 0
aerabi/lttt
"A Basis for Event-Driven Programming" based on Linear Temporal Type Theory
Language: Coq - Size: 81.1 KB - Last synced at: about 2 months ago - Pushed at: almost 4 years ago - Stars: 1 - Forks: 0
null-lambda/TAPL-hs
Haskell implementations of "Types and Programming Languages"
Language: Haskell - Size: 96.7 KB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 1 - Forks: 0
IlyaBizyaev/type-theory
Type Theory course homework (2019), ITMO University
Language: Haskell - Size: 181 KB - Last synced at: about 1 month ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 0
jiribenes/lily
Lily: A C++ linter based on linear types
Language: Haskell - Size: 444 KB - Last synced at: almost 2 years ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 0
pavponn/type-theory
Type Theory Course, ITMO University, 2019.
Language: Haskell - Size: 9.77 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0
ruza-net/kry
An experimental typechecker with dependent types, homogeneous path types, and cubical composition
Language: Rust - Size: 24.4 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0
DmytroMitin/hott-cubicaltt-exercises
Size: 4.88 KB - Last synced at: 3 months ago - Pushed at: over 6 years ago - Stars: 1 - Forks: 0
doofin/w-types
W types or well founded trees
Language: Idris - Size: 0 Bytes - Last synced at: 1 day ago - Pushed at: almost 7 years ago - Stars: 1 - Forks: 0
1jkunz1/Agda-Projects
Programming Language Concepts
Language: Agda - Size: 2.93 KB - Last synced at: over 1 year ago - Pushed at: almost 7 years ago - Stars: 1 - Forks: 0
Archimidis/TaPL
Haskell implementation of languages found in "Types and Programming Languages" book
Language: Haskell - Size: 33.2 KB - Last synced at: about 2 years ago - Pushed at: over 7 years ago - Stars: 1 - Forks: 0
bagnalla/PCF
A PCF interpreter in Haskell.
Language: Haskell - Size: 24.4 KB - Last synced at: about 3 hours ago - Pushed at: almost 8 years ago - Stars: 1 - Forks: 1
volgar1x/TSS
All Hail Patrou
Language: OCaml - Size: 61.5 KB - Last synced at: almost 2 years ago - Pushed at: about 8 years ago - Stars: 1 - Forks: 0
qradimir/tt-homework
Type Theory course homework
Language: Kotlin - Size: 103 KB - Last synced at: about 2 years ago - Pushed at: about 8 years ago - Stars: 1 - Forks: 0
kenpusney/type
Language: Racket - Size: 17.6 KB - Last synced at: about 2 months ago - Pushed at: almost 9 years ago - Stars: 1 - Forks: 0
pSub/tpl-notes
Language: TeX - Size: 133 KB - Last synced at: 2 months ago - Pushed at: about 11 years ago - Stars: 1 - Forks: 0
kaBeech/monads-are-easy
A brief cheatsheet for monads and related concepts
Size: 52.7 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 0
leo-leesco/Computational-logic-TD1
Typing a simple programming language
Language: OCaml - Size: 6.84 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0
bsdz/symbolize
Mathematical Symbol Engine
Language: Python - Size: 444 KB - Last synced at: 6 days ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0
lepton-lang/mltt-type-checker
An MLTT type checker implemented using Saki-Lang
Size: 7.81 KB - Last synced at: 3 months ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0
Church-of-Church-HSE/Church-of-Church-HSE.github.io
Church of Church project site
Language: Nix - Size: 908 KB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 0 - Forks: 1
iwilare/dinaturality
Agda proofs for the paper "Directed equality with dinaturality" (soon on arXiv and on my website)
Language: Agda - Size: 51.8 KB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 0 - Forks: 0
SyntakticSugar/babel
Personal blog about formal mathematics.
Language: HTML - Size: 53.7 KB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 0 - Forks: 0
wakame-tech/type-theory-rs
learn Type Theory in Rust
Language: Rust - Size: 203 KB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 0 - Forks: 0
JonasHoefer/poset-type-theory
Experimental implementation of a Cubical Type Theory modeled by presheaves over posets
Language: Haskell - Size: 366 KB - Last synced at: 12 months ago - Pushed at: 12 months ago - Stars: 0 - Forks: 1
yazaldefilimone/lambda-compiler.rs
Language: Rust - Size: 6.84 KB - Last synced at: 6 days ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0
yazaldefilimone/type-theory
Language: Agda - Size: 48.8 KB - Last synced at: 6 days ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0
yazaldefilimone/lambda-checker.agda
Language: Agda - Size: 1000 Bytes - Last synced at: 6 days ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0
vishallama/shapeless-guide-code Fork of underscoreio/shapeless-guide-code
Example code to accompany shapeless-guide.
Language: Scala - Size: 1020 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0
yazaldefilimone/lambda-calculus.ts
Untyped lambda calculus with bound variables.
Language: TypeScript - Size: 7.81 KB - Last synced at: 6 days ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0
yazaldefilimone/lambda-normalizer
seeking to understand patterns behind a normalizer for typed lambda calculus with type affinities.
Language: TypeScript - Size: 82 KB - Last synced at: 6 days ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0
kaicho8636/proposition_theory_python
Definitions and proofs written in Python
Language: Python - Size: 46.9 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
lean-ja/xena-ja
xena のいくつかの記事の非公式日本語訳を集めたものです
Size: 1.12 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
abdllahdev/lambda-calculus-for-all
[WIP] A series of tutorials for lambda calculus
Language: OCaml - Size: 3.22 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
Seasawher/math-in-type-theory-ja-old 📦
Mathematics in type theory の非公式日本語訳（古いです）
Size: 1.08 MB - Last synced at: 2 days ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
viniciusmiradouro/TheoremsInHaskell
I'm trying to use haskell as a proof checker. Simple.
Language: Haskell - Size: 11.7 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
wkolowski/LiTT
Moja prezentacja o Homotopicznej Teorii Typów na seminarium z Logiki i Teorii Typów
Language: TeX - Size: 18.6 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0
bridgekat/calculus-of-constructions
Lean 3 formalisation of bare-bones CC_ω (without inductive types).
Language: Lean - Size: 222 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0
ljdavns/software-fundations
All coq code and exercises from Software Fundations by Michael Clarkson.
Language: Coq - Size: 1.95 KB - Last synced at: almost 2 years ago - Pushed at: about 2 years ago - Stars: 0 - Forks: 0
typedefs/site
Typedefs website
Language: CSS - Size: 1.15 MB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 1
spencerhuston/Bant
Work-in-progess statically-typed, functional programming language made using Scala
Language: Scala - Size: 1020 KB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
wkolowski/Dependent-Types-and-Theorem-Proving
Slides and code snippets for a talk I have given in November 2021.
Language: TeX - Size: 7.89 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
aradarbel10/NbE
normalization by evaluation as a way of life
Language: Haskell - Size: 16.6 KB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
dfirsov/agda-programming-with-finite-sets
Dependently Typed Programming with Finite Sets
Language: Agda - Size: 35.2 KB - Last synced at: over 1 year ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0
dfirsov/agda-noetherianness
Variations on Noetherianness
Language: Agda - Size: 15.6 KB - Last synced at: over 1 year ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0
isaacazuelos/thir
Typing Haskell in Rust
Language: Rust - Size: 65.4 KB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0
Saisui/cat
Some math pages.
Size: 597 KB - Last synced at: almost 2 years ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0
sychoo/corewyvern
Language: Java - Size: 18.2 MB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0
VictorZXY/cst-part-ii-types-cheat-sheet
A cheet sheet for all the typing rules covered in the CST Part II Types course
Language: TeX - Size: 1010 KB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0
