elpinal/focused-modules elpinal/focused-modules

  • Stars
    star
    10
  • Rank 1,807,489 (Top 36 %)
  • Language Standard ML
  • License
    MIT License
  • Created about 4 years ago
  • Updated about 4 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
elpinal/focused-modules
github

elpinal

Reviews

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

Repository Details

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

More Repositories

1

bright-ml

A statically-typed programming language based on "F-ing modules"
Standard ML
79
star
2

modules

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

seqmod

Full implementation of F-ing Modules, with the power of sequent calculus
Standard ML
20
star
4

modules-rs

An interpreter of F-ing modules
Rust
18
star
5

subtyping-agda

Some rudimentary proofs on subtyping
Agda
11
star
6

mixml-sml

A MixML typechecker, written in Standard ML
Standard ML
10
star
7

tutor-ml-modules

Tutorial on implementing an ML-like module system
Rust
10
star
8

ucat

Univalent categories, displayed categories, and fibrations
Agda
10
star
9

types-1ml

Type systems written in 1ML
Roff
9
star
10

rain-ml

an abandoned project
Haskell
7
star
11

regions

Is it possible to extend region inference to System F?
Rust
7
star
12

capabilities

Capability Calculus for typed memory management [WIP]
Haskell
6
star
13

orthogonal-reflection

[WIP] Orthogonal-Reflection Construction
Agda
5
star
14

duploids

Duploids
Agda
5
star
15

types

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

twelf-proofs

Proofs for type systems and logical systems in Twelf
3
star
17

elt0

A typed assembly language for a virtual machine
Haskell
3
star
18

exsub-ccc

Categorical semantics of functional type theory with explicit substitutions
Agda
3
star
19

modal

Modal type system
Standard ML
3
star
20

canonical-singleton-kinds

Singleton kinds, hereditarily
Standard ML
2
star
21

regalloc

Training in register allocation
Idris
2
star
22

ellet-l

A linearly typed assembly language
Haskell
2
star
23

eval-order-poly-hs

Evaluation-order polymorphism
Haskell
2
star
24

lambda-nq

Lambda calculus with catch/throw
Standard ML
1
star
25

value-recursion-fs

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

typed-videocore

A typed assembly language for VideoCore IV [WIP]
1
star
27

emsh

An ordinary shell
Go
1
star
28

rain-vm

A virtual machine for Rain ML [WIP]
Rust
1
star
29

incr-cycle-detection

Incremental cycle detection implemented in Standard ML
Standard ML
1
star
30

well-founded-recursion

Well-founded recursion, written in Moscow ML
Standard ML
1
star
31

typed-assembly

Typed assembly language
Rust
1
star
32

wbt

Weight-balanced tree library for Standard ML
Standard ML
1
star
33

coc-forester

Bring `forester complete` to vim
TypeScript
1
star
34

coeffects

Analysis of context-dependence
Haskell
1
star
35

sml-lexer

A small lexer library for Standard ML
Standard ML
1
star
36

theb

A text-based web browser [WIP]
Haskell
1
star
37

fomega-typed-compilation

[WIP] Typed compilation of Fω
Haskell
1
star
38

types-bml

Type systems written in Bright ML
1
star