16 commits

Author	SHA1	Message	Date
Adam Chlipala	c611524a96	Prevent more warnings for Coq 8.10	2020-02-08 15:15:38 -05:00
Adam Chlipala	c5600db874	SubsetTypes	2017-03-21 19:27:36 -04:00
Adam Chlipala	1e7c33f0a9	Optimizing tactics for faster state-space exploration	2017-03-05 20:46:53 -05:00
Adam Chlipala	ef310e2b1e	SeparationLogic: soundness proof	2016-04-17 16:55:52 -04:00
Adam Chlipala	d5c82fa62e	Three new axioms in Map	2016-03-29 13:15:17 -04:00
Adam Chlipala	0845fa85b4	TypesAndMutation: type safety with garbage collection	2016-03-24 10:24:54 -04:00
Adam Chlipala	90e194c27e	Map.restrict	2016-03-24 08:28:53 -04:00
Adam Chlipala	2068f7691a	Moved some AbstractInterpretation working code into library	2016-03-05 16:07:11 -05:00
Adam Chlipala	c303dc02c9	AbstractInterpretation: analyzed one program	2016-03-05 15:56:15 -05:00
Adam Chlipala	e892c8dbab	AbstractInterpretation: proved a simulation and started using it	2016-03-05 15:17:41 -05:00
Adam Chlipala	d0d6b87a1d	More on AbstractInterpretation example; need to do a proper abstraction into a new trsys	2016-03-04 16:14:41 -05:00
Adam Chlipala	26023bdcb1	Start of AbstractInterpretation: interpret_sound	2016-03-04 14:00:34 -05:00
Adam Chlipala	a0487bc153	Add Map remove	2016-02-09 22:44:03 -05:00
Adam Chlipala	087e9334d8	Rename [map] to [fmap]	2016-02-09 09:07:37 -05:00
Adam Chlipala	ba3bb5c351	Interpreters: factorial example	2016-02-06 22:09:37 -05:00
Adam Chlipala	f8945106da	Start of BasicSyntax code	2015-12-31 15:44:34 -05:00