aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* 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 ↵JJ2024-06-29
| | | | whenever possible
* 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 ↵JJ2024-05-24
| | | | references
* 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
|
* implement the simply-typed lambda calculus with referencesJJ2024-05-22
|
* stlc-let: fixes to check/infer functionsJJ2024-05-15
|
* stlc-let: capture environments in closuresJJ2024-05-15
|
* stlc-let: implementation fixes & testsJJ2024-05-15
|
* implement the simply-typed lambda calculusJJ2024-05-15
|
* initial commitJJ2024-05-15