| Commit message (Expand) | Author | Age |
* | restructure code, put implementations into broadly categorical foldersHEADmain | JJ | 2024-10-24 |
* | refactor all implementations to use contracts | JJ | 2024-10-24 |
* | minor identifier changes | JJ | 2024-10-24 |
* | stlc-full: fix bug in context stratification | JJ | 2024-08-31 |
* | stlc-full: add tests | JJ | 2024-08-31 |
* | stlc-full: fix bugs | JJ | 2024-08-31 |
* | stlc-full: implement multisets | JJ | 2024-08-31 |
* | 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 |