elpinal/focused-modules

Stars
10
Rank 1,807,329 (Top 36 %)
Language Standard ML
License
MIT License
Created about 4 years ago
Updated about 4 years ago

elpinal/focused-modules

elpinal

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

A type system for ML-style modules, solving the avoidance problem by focusing [Crary 2020]

bright-ml

A statically-typed programming language based on "F-ing modules"

modules

Implementations of F-ing modules and 1ML, as well as bibliography of (mainly ML-style) modules

seqmod

Full implementation of F-ing Modules, with the power of sequent calculus

modules-rs

An interpreter of F-ing modules

subtyping-agda

Some rudimentary proofs on subtyping

mixml-sml

A MixML typechecker, written in Standard ML

tutor-ml-modules

Tutorial on implementing an ML-like module system

ucat

Univalent categories, displayed categories, and fibrations

types-1ml

Type systems written in 1ML

rain-ml

an abandoned project

regions

Is it possible to extend region inference to System F?

capabilities

Capability Calculus for typed memory management [WIP]

orthogonal-reflection

[WIP] Orthogonal-Reflection Construction

duploids

types

Type Systems: The rank 2 fragment of System F, linear types, kinds, and so on

twelf-proofs

Proofs for type systems and logical systems in Twelf

elt0

A typed assembly language for a virtual machine

exsub-ccc

Categorical semantics of functional type theory with explicit substitutions

modal

Modal type system

canonical-singleton-kinds

Singleton kinds, hereditarily

regalloc

Training in register allocation

ellet-l

A linearly typed assembly language

eval-order-poly-hs

Evaluation-order polymorphism

lambda-nq

Lambda calculus with catch/throw

value-recursion-fs

A type system for safe value recursion, written in F#

typed-videocore

A typed assembly language for VideoCore IV [WIP]

emsh

An ordinary shell

rain-vm

A virtual machine for Rain ML [WIP]

incr-cycle-detection

Incremental cycle detection implemented in Standard ML

well-founded-recursion

Well-founded recursion, written in Moscow ML

typed-assembly

Typed assembly language

wbt

Weight-balanced tree library for Standard ML

coc-forester

Bring `forester complete` to vim

coeffects

Analysis of context-dependence

sml-lexer

A small lexer library for Standard ML

theb

A text-based web browser [WIP]

fomega-typed-compilation

[WIP] Typed compilation of Fω

types-bml

Type systems written in Bright ML