index
:
mechanicals
main
Various implementations of the lambda calculus and friends.
git daemon user
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Collapse
)
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 ↵
JJ
2024-06-29
|
|
|
|
whenever possible
*
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 ↵
JJ
2024-05-24
|
|
|
|
references
*
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
|
[next]