| Commit message (Expand) | Author | Age |
|---|
| * | add self-contained implementation as stlc-full | JJ | 2024-08-31 |
| * | split lib into lib and base; move tests to separate files & directory | JJ | 2024-07-29 |
| * | stlc-dll, stlc-ext: split term and type equality | JJ | 2024-07-27 |
| * | backport check case reduction | JJ | 2024-07-27 |
| * | stlc-dll: cut back on cases and remove max-level | JJ | 2024-07-26 |
| * | stlc-dll: rewrite level-body and implement well-formed | JJ | 2024-07-26 |
| * | backport check refactorings | JJ | 2024-07-16 |
| * | backport interpret-/infer-/check- renaming and remove implicit params | JJ | 2024-07-15 |
| * | stlc-dll: rework infer and check to operate on and return normalized types | JJ | 2024-07-04 |
| * | stlc-dll: rename interpret-, remove optional parameters | JJ | 2024-07-04 |
| * | stlc-dll: reduce annotations on tests, reimplement doubly linked lists | JJ | 2024-06-29 |
| * | stlc-dll: add back check cases, inline and fix replace, implement well-formed | JJ | 2024-06-29 |
| * | stlc-dll: rename infer- and check- | JJ | 2024-06-29 |
| * | stlc-dll: significantly reduce cases in check by calling over to infer whenev... | JJ | 2024-06-29 |
| * | stlc-dll: require inl/inr to be externally annotated | JJ | 2024-06-28 |
| * | stlc-dll: expand types properly, support unannotated folds, write tests | JJ | 2024-06-24 |
| * | stlc-ext, stlc-rec: backport bug fixes | JJ | 2024-06-24 |
| * | stlc-dll: major bugfixes | JJ | 2024-06-24 |
| * | broadly switch to infix operators | JJ | 2024-06-21 |
| * | stlc-dll: initial implementation | JJ | 2024-06-20 |
| * | stlc-ext: conditional fixes and tests | JJ | 2024-06-20 |
| * | stlc-ext: ascryption fixes | JJ | 2024-06-20 |
| * | go all in on unicode: rename ctx and heap to \Gamma and \Sigma | JJ | 2024-06-20 |
| * | stlc-ext: typecheck boolean and natural operations | JJ | 2024-06-20 |
| * | add some typing rules, minor fixes | JJ | 2024-06-20 |
| * | stlc-rec: initial implementation | JJ | 2024-06-20 |
| * | implement the simply-typed lambda calculus with impredicative refs | JJ | 2024-06-17 |
| * | implement the simply-typed lambda calculus with general recursion (fix) | JJ | 2024-06-17 |
| * | stlc-ext: add primitive operations on booleans and naturals | JJ | 2024-06-17 |
| * | update readme | JJ | 2024-06-16 |
| * | implement the simply-typed lambda calculus with simple extensions | JJ | 2024-06-16 |
| * | stlc-*: do not throw errors within check | JJ | 2024-06-15 |
| * | stlc-let: reimplement | JJ | 2024-06-15 |
| * | implement the standard simply-typed lambda calculus | JJ | 2024-06-15 |
| * | lib: fix bug in desugaring match | JJ | 2024-06-15 |
| * | stlc-pred: clean up code | JJ | 2024-06-15 |
| * | stlc-pred: use stlc-ref interpret impl | JJ | 2024-06-15 |
| * | stlc-ref: rewrite, add type checker | JJ | 2024-06-15 |
| * | lib: provide desugaring function | JJ | 2024-06-08 |
| * | lib: provide fmt and strip functions | JJ | 2024-06-08 |
| * | stld-pred: bugfixes | JJ | 2024-06-05 |
| * | stlc-pred: rewrite to follow typing rules directly | JJ | 2024-05-29 |
| * | implement the simply-typed lambda calculus with typechecked predicative refer... | JJ | 2024-05-24 |
| * | implement various combinators in terms of the lambda calculus | JJ | 2024-05-22 |
| * | lc: implement α-conversion and β-reduction separately | JJ | 2024-05-22 |
| * | lc, stlc-let: rewrite interpreter | JJ | 2024-05-22 |
| * | readme: add description | JJ | 2024-05-22 |
| * | implement the simply-typed lambda calculus with references | JJ | 2024-05-22 |
| * | stlc-let: fixes to check/infer functions | JJ | 2024-05-15 |
| * | stlc-let: capture environments in closures | JJ | 2024-05-15 |
