aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* stlc-full: add testsJJ2024-08-31
* stlc-full: fix bugsJJ2024-08-31
* stlc-full: implement multisetsJJ2024-08-31
* add self-contained implementation as stlc-fullJJ2024-08-31
* split lib into lib and base; move tests to separate files & directoryJJ2024-07-29
* stlc-dll, stlc-ext: split term and type equalityJJ2024-07-27
* backport check case reductionJJ2024-07-27
* stlc-dll: cut back on cases and remove max-levelJJ2024-07-26
* stlc-dll: rewrite level-body and implement well-formedJJ2024-07-26
* backport check refactoringsJJ2024-07-16
* backport interpret-/infer-/check- renaming and remove implicit paramsJJ2024-07-15
* stlc-dll: rework infer and check to operate on and return normalized typesJJ2024-07-04
* stlc-dll: rename interpret-, remove optional parametersJJ2024-07-04
* stlc-dll: reduce annotations on tests, reimplement doubly linked listsJJ2024-06-29
* stlc-dll: add back check cases, inline and fix replace, implement well-formedJJ2024-06-29
* stlc-dll: rename infer- and check-JJ2024-06-29
* stlc-dll: significantly reduce cases in check by calling over to infer whenev...JJ2024-06-29
* stlc-dll: require inl/inr to be externally annotatedJJ2024-06-28
* stlc-dll: expand types properly, support unannotated folds, write testsJJ2024-06-24
* stlc-ext, stlc-rec: backport bug fixesJJ2024-06-24
* stlc-dll: major bugfixesJJ2024-06-24
* broadly switch to infix operatorsJJ2024-06-21
* stlc-dll: initial implementationJJ2024-06-20
* stlc-ext: conditional fixes and testsJJ2024-06-20
* stlc-ext: ascryption fixesJJ2024-06-20
* go all in on unicode: rename ctx and heap to \Gamma and \SigmaJJ2024-06-20
* stlc-ext: typecheck boolean and natural operationsJJ2024-06-20
* add some typing rules, minor fixesJJ2024-06-20
* stlc-rec: initial implementationJJ2024-06-20
* implement the simply-typed lambda calculus with impredicative refsJJ2024-06-17
* implement the simply-typed lambda calculus with general recursion (fix)JJ2024-06-17
* stlc-ext: add primitive operations on booleans and naturalsJJ2024-06-17
* update readmeJJ2024-06-16
* implement the simply-typed lambda calculus with simple extensionsJJ2024-06-16
* stlc-*: do not throw errors within checkJJ2024-06-15
* stlc-let: reimplementJJ2024-06-15
* implement the standard simply-typed lambda calculusJJ2024-06-15
* lib: fix bug in desugaring matchJJ2024-06-15
* stlc-pred: clean up codeJJ2024-06-15
* stlc-pred: use stlc-ref interpret implJJ2024-06-15
* stlc-ref: rewrite, add type checkerJJ2024-06-15
* lib: provide desugaring functionJJ2024-06-08
* lib: provide fmt and strip functionsJJ2024-06-08
* stld-pred: bugfixesJJ2024-06-05
* stlc-pred: rewrite to follow typing rules directlyJJ2024-05-29
* implement the simply-typed lambda calculus with typechecked predicative refer...JJ2024-05-24
* implement various combinators in terms of the lambda calculusJJ2024-05-22
* lc: implement α-conversion and β-reduction separatelyJJ2024-05-22
* lc, stlc-let: rewrite interpreterJJ2024-05-22
* readme: add descriptionJJ2024-05-22