Propositions as Types, with Howard on Curry-Howard
Propositions as Types
Draft, 29 November 2014
The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery.Comments still solicited!
Tuesday 25 November at The Stand Comedy Club, I will be part of the line up at Bright Club, speaking on the subject of 'Turingery'. Bright Club is stand-up by academics---we are trained professionals; don't try this at home! Doors open 7:30pm, show starts 8:30pm. The Stand is at 5 York Place, Edinburgh, EH1 3EB. Tickets £5 at the door or online.
Kickstarter-like, OurScreen will arrange to show a film if enough people sign up to see it. I've scheduled a showing:
Cameo Edinburgh, 12 noon, Tuesday 2 December 2015
cost: £6.80 Book tickets from OurScreen.
If 34 people sign up by Sunday 23 November, then the showing will go ahead.
Save our Universities
this forward as a campaign are solicited.
Dear Gavin Brown, Sarah Boyack, Alison Johnstone, Kezia Dugdale, Cameron Buchanan and Neil Findlay, I write to ask your help to preserve a secure future for Scottish Universities. Academics for all UK universities, including those in Scotland, have faced falling wages and falling pensions over many years. "The real wages of academics have fallen by 13% since 2008, one of the largest sustained wage cuts any profession has suffered since the Second World War." So wrote Will Hutton in the Guardian, October 2013 . In 2011, Universities UK imposed vastly reduced pensions on new hires. Old hires who pay into the pension fund for forty years receive a pension of one-half their final salary; new hires who do the same receive a pension of one-half their average salary. Basing pensions on average rather than final salary may be sensible, but to do so with no adjustment in multiplier suggests employers are using this as an excuse to slip in a large cut; it means new hires receive about 2/3 the benefits received by old hires. All staff also suffered other cuts to pensions: additional caps and less good adjustment for inflation. At the time, it was predicted that within a few years old hires would be moved to the inferior scheme for new hires, and that is what has now come to pass.  Universities UK argue that the reductions are necessary to avoid a deficit, but their claim has been widely criticised. Notably, a group of prominent statisticians point out Universities UK inflated the deficit by assuming a buoyant economy when predicting future salaries but assuming a recession when predicting investment returns.  A strong university system is one of the jewels in the crown of the UK, and particularly for Scotland. That excellence is a huge driver of innovation and growth. If Scotland reduces its investment in universities, it won't be long before we feel that loss throughout the economy. [4,5] Scotland has a University system second to none, and to keep it strong we need pay and pensions that attract and retain the best minds throughout the world. We must have a system that is fair to both: old hires must retain attractive conditions; new hires must have the bad deal imposed on them in 2011 rolled back. Speaking as an old hire, I'd settle for a small cut in pension if it meant bringing new hires onto the same level: we must keep the system strong for the future. The UCU has gone on strike over the issue (suspension of assessment, which it hopes will minimise disruption for students). But UCU is unlikely to succeed without political support. I write to ask you, as my representative in the Scottish parliament, will you direct the Scottish Funding Council to make fair treatment for academics in Scottish Universities, both new hires and old, a top priority? Thank you for your consideration. Yours, -- Philip Wadler Professor of Theoretical Computer Science School of Informatics University of Edinburgh  http://www.theguardian.com/commentisfree/2013/oct/13/england-leave-funding-universities-students  http://www.theguardian.com/education/2010/nov/23/oxbridge-pensions-academics-protest-united  http://www.theguardian.com/higher-education-network/blog/2014/oct/29/marking-boycott-why-are-academics-protesting-about-pensions  http://www.universities-scotland.ac.uk/index.php?mact=News,cntnt01,detail,0&cntnt01articleid=156&cntnt01returnid=23  Royal Society of Edinburgh, Enlightening the Constitutional Debate, Science and Higher Education, p177--198, http://www.royalsoced.org.uk/cms/files/events/reports/2013-2014/The%20Book.pdf