Pinned Repositories
bright-ml
A statically-typed programming language based on "F-ing modules"
focused-modules
A type system for ML-style modules, solving the avoidance problem by focusing [Crary 2020]
mixml-sml
A MixML typechecker, written in Standard ML
modules
Implementations of F-ing modules and 1ML, as well as bibliography of (mainly ML-style) modules
modules-rs
An interpreter of F-ing modules
seqmod
Full implementation of F-ing Modules, with the power of sequent calculus
subtyping-agda
Some rudimentary proofs on subtyping
tutor-ml-modules
Tutorial on implementing an ML-like module system
types-1ml
Type systems written in 1ML
ucat
Univalent categories, displayed categories, and fibrations
elpinal's Repositories
elpinal/elt0
A typed assembly language for a virtual machine
elpinal/ellet-l
A linearly typed assembly language
elpinal/coeffects
Analysis of context-dependence
elpinal/theb
A text-based web browser [WIP]
elpinal/typed-assembly
Typed assembly language
elpinal/typed-videocore
A typed assembly language for VideoCore IV [WIP]
elpinal/benchmarks
A collection of benchmarks
elpinal/cc
An implementation of the Calculus of Constructions
elpinal/cciiff
elpinal/coco3-go-to-bed-by9
elpinal/definitional-type-reduction
What is Definitional Type Reduction?
elpinal/dlm
Download to structured path
elpinal/explicit-substitution
λσ-calculus
elpinal/git-factory
Not so bad
elpinal/lakka
A programming language targeting ELT0 [WIP]
elpinal/license
Generate LICENSE file you want
elpinal/lioll
elpinal/lit-qulit
An advanced shell
elpinal/mdindicator
Markdown indicator
elpinal/moon-stack
Coming soon
elpinal/mtal
A modular module system for typed assembly languages, or “how to implement modular typed assembly languages?”
elpinal/ocaml-modular-implicits
OCaml extended with modular implicits
elpinal/ottoriono
A minimal language
elpinal/parse-and-substitution
Parse (not just transform) named λ-terms "directly" into nameless ones
elpinal/test-contria
How test should be written?
elpinal/thc
The third Elacht Compiler [WIP]
elpinal/types-clj
Types in Clojure
elpinal/types-hs
Bounded quantification, explicit substitutions, type classes, label-selective λ-calculus, and open existential types
elpinal/types-scala
Type inference and polymorphic types
elpinal/vvmn
Manage various versions of Vim