User Activity
-
Modified
a comment
on
discussion Extensions for SASyLF
on
SASyLF
One of the more confusing things with proofs and with SASyLF is that a successful...
-
Posted
a comment
on
discussion Extensions for SASyLF
on
SASyLF
One of the more confusing things with proofs and with SASyLF is that a successful...
-
Posted
a comment
on
discussion Extensions for SASyLF
on
SASyLF
To prove individual derivations coinductively, one can use d: ... by coinduction...
-
Posted
a comment
on
discussion Extensions for SASyLF
on
SASyLF
Basic coinduction should be a nice addition to SASyLF: Coinductive rules: t1 ⇑ =======...
-
Posted
a comment
on
discussion Extensions for SASyLF
on
SASyLF
An easy way forward is to not complain about the lack of an assumption rule for a...
-
Posted
a comment
on
discussion Extensions for SASyLF
on
SASyLF
So it would be nice to define different kinds of contexts: Gamma one-variable-and-no-nonterminals...
-
Posted
a comment
on
discussion Extensions for SASyLF
on
SASyLF
Currently in SASyLF, the form of contexts is Gamma ::= only-terminals | Gamma one-variable-and-other-normal-nonterminals...
-
Posted
a comment
on
discussion Extensions for SASyLF
on
SASyLF
do case analysis on ... end case analysis is implemented. This new syntax doesn't...
Personal Data
- Username:
- boyland
- Joined:
- 2003-10-27 22:16:43
Projects
This is a list of open source software projects that John Tang Boyland is associated with:
-
SASyLF SASyLF is an proof assistant for reasoning about programs. Last Updated:
