CALL FOR WORKSHOPS, TUTORIALS, SYSTEM COMPETITIONS, AND PAPERS
25th International Conference on Automated Deduction (CADE-25)
Berlin, Germany, 1-7 August 2015
http://www.cade-25.info
Submission deadlines:
14
FIRST CALL FOR PAPERS
Thirteenth International Conference on
TYPED LAMBDA CALCULI AND APPLICATIONS (TLCA 2015)
1 July - 3 July 2015, Warsaw, Poland
(co-located with RTA 2015 as part of RDP 2015)
Seems a good idea to me. Given ETA_AX, it's easy to show equivalence with
current HOL Light, and it's always better to have closed formulae coming out
of definition commands.
One small point: the formulae as written in the linked message do not have
the intended syntactic form (due to
The commands that set them up as syntax should also set up the standard TeX
override map to do this. For example, boolScript.sml includes the following
lines to set up if-then-else:
val _ = TeX_notation {hol = if, TeX = (\\HOLKeyword{if}, 2)}
val _ = TeX_notation {hol = then, TeX =
