elpinal

Abstract behavior

Pinned Repositories

bright-ml
A statically-typed programming language based on "F-ing modules"
Language:Standard ML79 3 11
focused-modules
A type system for ML-style modules, solving the avoidance problem by focusing [Crary 2020]
Language:Standard ML10 2 00
mixml-sml
A MixML typechecker, written in Standard ML
Language:Standard ML10 1 00
modules
Implementations of F-ing modules and 1ML, as well as bibliography of (mainly ML-style) modules
Language:Haskell27 3 20
modules-rs
An interpreter of F-ing modules
Language:Rust18 1 00
seqmod
Full implementation of F-ing Modules, with the power of sequent calculus
Language:Standard ML20 2 00
subtyping-agda
Some rudimentary proofs on subtyping
Language:Agda11 2 01
tutor-ml-modules
Tutorial on implementing an ML-like module system
Language:Rust10 1 00
types-1ml
Type systems written in 1ML
Language:Roff9 1 00
ucat
Univalent categories, displayed categories, and fibrations
Language:Agda9 2 00

elpinal's Repositories

elpinal/modules
Implementations of F-ing modules and 1ML, as well as bibliography of (mainly ML-style) modules
Language:Haskell27 3 20
elpinal/seqmod
Full implementation of F-ing Modules, with the power of sequent calculus
Language:Standard ML20 2 00
elpinal/subtyping-agda
Some rudimentary proofs on subtyping
Language:Agda11 2 01
elpinal/focused-modules
A type system for ML-style modules, solving the avoidance problem by focusing [Crary 2020]
Language:Standard ML10 2 00
elpinal/mixml-sml
A MixML typechecker, written in Standard ML
Language:Standard ML10 1 00
elpinal/tutor-ml-modules
Tutorial on implementing an ML-like module system
Language:Rust10 1 00
elpinal/ucat
Univalent categories, displayed categories, and fibrations
Language:Agda9 2 00
elpinal/duploids
Duploids
Language:Agda5 1 0
elpinal/orthogonal-reflection
[WIP] Orthogonal-Reflection Construction
Language:Agda5 2 0
elpinal/exsub-ccc
Categorical semantics of functional type theory with explicit substitutions
Language:Agda3 2 0
elpinal/modal
Modal type system
Language:Standard ML3 1 0
elpinal/twelf-proofs
Proofs for type systems and logical systems in Twelf
3 1 0
elpinal/canonical-singleton-kinds
Singleton kinds, hereditarily
Language:Standard ML2 1 0
elpinal/coc-forester
Bring `forester complete` to vim
Language:TypeScript1 1 0
elpinal/config
My configuration files
Language:Vim Script1 1 0
elpinal/emsh
An ordinary shell
Language:Go1 1 0
elpinal/incr-cycle-detection
Incremental cycle detection implemented in Standard ML
Language:Standard ML1 1 0
elpinal/lambda-nq
Lambda calculus with catch/throw
Language:Standard ML1 1 0
elpinal/sml-lexer
A small lexer library for Standard ML
Language:Standard ML1 1 0
elpinal/wbt
Weight-balanced tree library for Standard ML
Language:Standard ML1 1 0
elpinal/agda-categories
A new Categories library for Agda
Language:Agda1 0
elpinal/agda-proofs
My playground for Agda proofs
Language:Agda1 0
elpinal/emacs-config
My Emacs configurations.
Language:Emacs Lisp1 0
elpinal/forester.vim
A basic vim plugin for forester
Language:Vim Script1 0
elpinal/hamlet
SML reference interpreter
Language:Standard ML
elpinal/isabelle-hol-proofs
My playground for Isabelle/HOL
Language:Isabelle
elpinal/keepsake
Browsing history, curated.
Language:Go1 0
elpinal/remark-code-extra
Add to or transform the HTML output of markdown code blocks using remark
Language:TypeScript
elpinal/SATySFi
A statically-typed, functional typesetting system
Language:OCaml
elpinal/sml-personal-lib
My personal library for Standard ML
Language:Standard ML1 0