git.megacz.com Git - coq-hetmet.git/shortlog

2011-05-31	Adam Megacz	update for new GHC coercion representation	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	remove RLet and RWhere	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	let RCut take a left environment as well	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	use -fsimpleopt-before-flatten in sanity checks	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	remove RJoin rule	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	better error reporting in coreTypeToWeakType; dont...	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	Makefile: use a for-loop to compile sanity checks	commit \| commitdiff \| tree \| snapshot
2011-05-30	Adam Megacz	add "sanity" target to Makefile	commit \| commitdiff \| tree \| snapshot
2011-05-30	Adam Megacz	add -fflatten and -funsafe-skolemize flags	commit \| commitdiff \| tree \| snapshot
2011-05-29	Adam Megacz	add RCut, RLeft, RRight rules	commit \| commitdiff \| tree \| snapshot
2011-05-28	Adam Megacz	rename constructors of Arrange to start with A instead...	commit \| commitdiff \| tree \| snapshot
2011-05-28	Adam Megacz	move more arrange routines into NaturalDeductionContext	commit \| commitdiff \| tree \| snapshot
2011-05-28	Adam Megacz	move Arrange into NaturalDeductionContext	commit \| commitdiff \| tree \| snapshot
2011-05-28	Adam Megacz	migrate HaskStrong away from using LeveledHaskType	commit \| commitdiff \| tree \| snapshot
2011-05-27	Adam Megacz	HaskProof: make the succedent level part of the judgment	commit \| commitdiff \| tree \| snapshot
2011-05-27	Adam Megacz	update Demo.hs	commit \| commitdiff \| tree \| snapshot
2011-05-27	Adam Megacz	add commented-out/incomplete implementation of simplify...	commit \| commitdiff \| tree \| snapshot
2011-05-27	Adam Megacz	General.v: add boolean and/or functions	commit \| commitdiff \| tree \| snapshot
2011-05-27	Adam Megacz	rename variables to avoid Coq pickiness during extraction	commit \| commitdiff \| tree \| snapshot
2011-05-27	Adam Megacz	partial support for LetRec in flattener	commit \| commitdiff \| tree \| snapshot
2011-05-26	Adam Megacz	fix types of GAS_loop{l,r}	commit \| commitdiff \| tree \| snapshot
2011-05-26	Adam Megacz	add new Where rule, eliminate unnecessary ga_swaps...	commit \| commitdiff \| tree \| snapshot
2011-05-26	Adam Megacz	note to self in HaskWeak	commit \| commitdiff \| tree \| snapshot
2011-05-23	Adam Megacz	NaturalDeduction: add nd_exch	commit \| commitdiff \| tree \| snapshot
2011-05-16	Adam Megacz	HaskFlattener: support escapifying multi-leaf contexts	commit \| commitdiff \| tree \| snapshot
2011-05-16	Adam Megacz	complete rewrite of GArrowTikZ, update examples	commit \| commitdiff \| tree \| snapshot
2011-05-16	Adam Megacz	GArrowSkeleton: add some more optimization cases	commit \| commitdiff \| tree \| snapshot
2011-05-16	Adam Megacz	GArrowPortShape: add detectShape	commit \| commitdiff \| tree \| snapshot
2011-05-16	Adam Megacz	Unify.hs: commenting fix	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	add begin/end{preview} to tex output	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	GArrowTikZ: improve pdf page cropping	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	update demo for new more-efficient encoding of functions	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	more efficient encoding of function types	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	add an identity production for Arrange	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	update demo	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	add GArrowPortShape	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	add GArrowSkeleton	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	fix bug in flattener, make extensionality axiom explicit	commit \| commitdiff \| tree \| snapshot
2011-05-14	Adam Megacz	update examples	commit \| commitdiff \| tree \| snapshot
2011-05-14	Adam Megacz	integrate skolemization pass with flattening	commit \| commitdiff \| tree \| snapshot
2011-05-14	Adam Megacz	improve detection of type function kinds, mainly their...	commit \| commitdiff \| tree \| snapshot
2011-05-14	Adam Megacz	add split_list to General.v	commit \| commitdiff \| tree \| snapshot
2011-05-14	Adam Megacz	add ToString instance for lists	commit \| commitdiff \| tree \| snapshot
2011-05-13	Adam Megacz	first draft of skolemization pass	commit \| commitdiff \| tree \| snapshot
2011-05-13	Adam Megacz	add EqDecidable instances for option and Tree	commit \| commitdiff \| tree \| snapshot
2011-05-12	Adam Megacz	swap order of hypotheses in RApp to match RLet	commit \| commitdiff \| tree \| snapshot
2011-05-12	Adam Megacz	rewrite {take,drop}_arg_types to avoid use of equality...	commit \| commitdiff \| tree \| snapshot
2011-05-12	Adam Megacz	HaskFlattener: represent first-order abstraction using...	commit \| commitdiff \| tree \| snapshot
2011-05-12	Adam Megacz	HaskFlattener: use ga_mk_raw	commit \| commitdiff \| tree \| snapshot
2011-05-12	Adam Megacz	update PCF.v for new ECKind	commit \| commitdiff \| tree \| snapshot
2011-05-12	Adam Megacz	HaskFlattener: simplify the flattener	commit \| commitdiff \| tree \| snapshot
2011-05-12	Adam Megacz	HaskStrongTypes: add {take,drop}_arg_types	commit \| commitdiff \| tree \| snapshot
2011-05-11	Adam Megacz	HaskFLattener: formatting fixes and refactoring	commit \| commitdiff \| tree \| snapshot
2011-05-10	Adam Megacz	start using type-family-based GArrow classes	commit \| commitdiff \| tree \| snapshot
2011-05-10	Adam Megacz	have Makefile check for coq 8.3pl2-tracer	commit \| commitdiff \| tree \| snapshot
2011-05-10	Adam Megacz	add examples/.build to gitignore	commit \| commitdiff \| tree \| snapshot
2011-05-10	Adam Megacz	add support for flattening non-recursive Let bindings	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	move general-purpose routines from HaskFlattener to...	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	split HaskLiteralsAndTyCons into two files	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	add support for hetmet_unflatten	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	add Demo.hs	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	make GArrowTikZ into a module rather than a standalone...	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	add support for hetmet_flatten casting variable	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	allow -fcoqpass to change the type of top-level bindings	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	use the "debug" version of Outputable for ToString...	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	change ECKind to =>=>*	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	abstract out the kind of environment classifiers (ECKind)	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	major improvements to flattener; almost finished now	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	allow rank-1 polymorphic types for globals	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	add PairTyCon and UnitTyCon	commit \| commitdiff \| tree \| snapshot
2011-05-09	Adam Megacz	minor cleanups to Extraction-prefix.hs to eliminate...	commit \| commitdiff \| tree \| snapshot
2011-05-05	Adam Megacz	further improvements to flattener	commit \| commitdiff \| tree \| snapshot
2011-05-03	Adam Megacz	separate HaskProofStratified into PCF.v, HaskProgrammin...	commit \| commitdiff \| tree \| snapshot
2011-04-30	Adam Megacz	reorganize HaskProof files	commit \| commitdiff \| tree \| snapshot
2011-04-30	Adam Megacz	clean up hints for NaturalDeduction, split ProgrammingL...	commit \| commitdiff \| tree \| snapshot
2011-04-29	Adam Megacz	remove many [[admit]]s from HaskProofFlattener.v	commit \| commitdiff \| tree \| snapshot
2011-04-27	Adam Megacz	Merge branch 'master' of git.megacz.com/coq-hetmet	commit \| commitdiff \| tree \| snapshot
2011-04-27	Adam Megacz	prove all [admit]ted lemmas in HaskStrongToProof (not...	commit \| commitdiff \| tree \| snapshot
2011-04-26	Adam Megacz	add Makefile target for tikz demo	commit \| commitdiff \| tree \| snapshot
2011-04-26	Adam Megacz	add examples/Makefile	commit \| commitdiff \| tree \| snapshot
2011-04-25	Adam Megacz	add -fno-warn-unused-{binds,patterns} to Coq extraction	commit \| commitdiff \| tree \| snapshot
2011-04-25	Adam Megacz	update GArrowTikZ.hs; still not finished, though	commit \| commitdiff \| tree \| snapshot
2011-04-25	Adam Megacz	remove ClosedSIND (use "SIND []" instead)	commit \| commitdiff \| tree \| snapshot
2011-04-24	Adam Megacz	remove all admits from ProgrammingLanguage.v	commit \| commitdiff \| tree \| snapshot
2011-04-24	Adam Megacz	NaturalDeduction: add nd_swap, nd_prod_split, and some...	commit \| commitdiff \| tree \| snapshot
2011-04-24	Adam Megacz	add examples targets to Makefile	commit \| commitdiff \| tree \| snapshot
2011-04-24	Adam Megacz	add Unify.hs to examples	commit \| commitdiff \| tree \| snapshot
2011-04-18	Adam Megacz	speed up builds by removing some dependencies from...	commit \| commitdiff \| tree \| snapshot
2011-04-16	Adam Megacz	fix erroneous conclusion to penultimate lemma	commit \| commitdiff \| tree \| snapshot
2011-04-11	Adam Megacz	use the $(MAKE) variable so -j2 works	commit \| commitdiff \| tree \| snapshot
2011-04-11	Adam Megacz	Merge branches 'master' and 'master' of git.megacz...	commit \| commitdiff \| tree \| snapshot
2011-04-11	Adam Megacz	unbreak lots more stuff	commit \| commitdiff \| tree \| snapshot
2011-04-11	Adam Megacz	uncomment some code in ProgrammingLanguage.v	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	remove the very last admit (missing proof) from General...	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	add skeleton of GArrowTikZ	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	separate CoqPass.hs from All.v in Makefile	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	fix bug in GeneralizedArrowFromReification	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	All.v: uncomment things	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	bugfix in ReificationsIsomorphicToGeneralizedArrows	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	add commented-out definitions for analytic proofs and...	commit \| commitdiff \| tree \| snapshot
next

Coq proofs and code accompanying the HetMet extensions for GHC

RSS Atom