yellowsquid/church-eval.git - [no description]

Age	Commit message (Collapse)	Author
2023-07-03	Add literals as primitive term.	Chloe Brown

2023-06-22	Add encodings for containers.	Chloe Brown
	Remove useless junk.
2023-06-21	Add sums, vectors and arithmetic encodings.	Chloe Brown
	Also define pretty printing of terms.
2023-06-16	Define semantics and encode types up to pairs.	Chloe Brown

2023-06-16	Reset using only co-de Bruijn syntax.	Chloe Brown

2023-06-09	Use co-deBruijn syntax in logical relation proof.master	Chloe Brown
	Many proofs are still missing. Because they are erased, the program still runs fine without them.
2023-06-08	Use CoDebruijn syntax at top level.	Chloe Brown

2023-06-08	Fully expand thinnings.	Chloe Brown
	This makes adding CoDebruijn syntax simpler. If carrying the lengths of contexts around is too inefficient, I can always switch back to truncated thinnings.
2023-06-06	Add a pretty printer.	Chloe Brown

2023-06-06	Write an encoding for data types.	Chloe Brown

2023-06-01	Give a logical relation template.	Chloe Brown

2023-06-01	Define terms with substitution as an operation.	Chloe Brown

2023-06-01	Add some properties of thinnings.	Chloe Brown

2023-05-24	Give a defunctionalised fuel-powered interpreter.	Chloe Brown

2023-05-24	Make normal forms a property.	Chloe Brown
	Weakening is now part of eval.
2023-05-24	Make things less disgusting.	Chloe Brown

2023-05-23	Merge mutual definitions into a single function.	Chloe Brown
	This is really bad style, but a useful step in making a fuel-powered stack-based interpreter.
2023-05-23	Use the continuation monad.	Chloe Brown

2023-05-23	Define a partial evaluator inductively.	Chloe Brown

2023-05-23	Define terms and thinnings.	Chloe Brown