[TYPES/announce] Participate: Enabling Domain Experts to use Formalised Reasoning (AISB 2013, Exeter, UK, 3-5 Apr 2013). Tutorials on Matching, Auctions, Finance.

[Christoph LANGE]

(How does this relate to types?  Well, some submissions explicitly
discuss whether or not to use types when formalising, or what types to
use.  Particularly the submissions on auction theory do so.)

Do-Form: Enabling Domain Experts to use Formalised Reasoning
http://cs.bham.ac.uk/research/projects/formare/events/aisb2013

CALL FOR PARTICIPATION

Symposium at the annual convention of the
AISB (Society for the Study of
  Artificial Intelligence and Simulation of Behaviour;
  http://www.aisb.org.uk)
University of Exeter, UK
3-5 April 2013
http://emps.exeter.ac.uk/computer-science/research/aisb/
(early registration deadline 5 March)

HANDS-ON TUTORIAL SESSIONS (details below) with
* M. Utku Ünver (matching markets)
* Peter Cramton (auctions)
* Neels Vosloo (finance markets regulation)
(http://www.cs.bham.ac.uk/research/projects/formare/events/aisb2013/invited.php)

PAPER and DEMO PRESENTATIONS on
* environmental models
* controlled natural languages
* ontologies
* auction theory
* software verification
* formal specification
* autonomous systems
* self-explaining systems
(http://www.cs.bham.ac.uk/research/projects/formare/events/aisb2013/proceedings.php)

This symposium is motivated by the long-term VISION of making information
systems dependable.  In the past even mis-represented units of
measurements caused fatal ENGINEERING disasters.  In ECONOMICS, the
subtlety of issues involved in good auction design may have led to low
revenues in auctions of public goods such as the 3G radio spectra.
Similarly, banks' value-at-risk (VaR) models – the leading method of
financial risk measurement – are too large and change too quickly to be
thoroughly vetted by hand, the current state of the art; in the London
Whale incident of 2012, JP Morgan claimed that its exposures were $67mn
under one of its VaR models, and $129 under another one.  Verifying a
model's properties requires formally specifying them; for VaR models, any
work would have to start with this most basic step, as regulators' current
desiderata are subjective and ambiguous.

We believe that these problems can be addressed by representing the
knowledge underlying such models and mechanisms in a formal, explicit,
machine-verifiable way.  Contemporary computer science offers a wide
choice of knowledge representation languages well supported by
verification tools.  Such tools have been successfully applied, e.g., for
verifying software that controls commuter rail or payment systems.  Still,
DOMAIN EXPERTS without a strong computer science background find it
challenging to choose the right tools and to use them.  This symposium
aims at investigating ways to support them.  Some problems can be
addressed now, others will bring new challenges to computer science.

THE SYMPOSIUM is designed to bring domain experts and formalisers into
close and fruitful contact with each other: domain experts will be able to
present their fields and problems to formalisers; formalisers will be
exposed to new and challenging problem areas. We will combine talks and
hands-on sessions to ensure close interaction among participants from both
sides.

World-class economists will offer HANDS-ON TUTORIAL SESSIONS on the
following topics:

* MATCHING MARKETS (M. Utku Ünver, Boston College): These include matching
  students to schools, interns to hospitals, and kidney donors to
  recipients. See the documentation for the 2012 Nobel Memorial Prize in
  Economic Sciences for more background information.

* AUCTIONS (Peter Cramton, University of Maryland): Peter has been working
  on auctions for Ofcom UK (4G spectrum auction), the UK Department of the
  Environment and Climate Change, and others – and most recently on the
  “applicant auctions” for the new top-level Internet domains issued by the
  ICANN.

* FINANCE MARKETS REGULATION (Neels Vosloo, Financial Services Authority,
  UK): It is currently impossible for regulators to properly inspect risk
  management models. Test portfolios are a promising tool for identifying
  problems with risk management models. To what extent can techniques from
  mechanised reasoning automate some of the inspection process?

COMMENTS/QUESTIONS/ENQUIRIES to be sent to DoForm2013 at easychair.org

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ SePublica Workshop @ ESWC 2013.  Montpellier, France, 26-30 May.
  Deadline 4 Mar; http://sepublica.mywikipaper.org
→ Intelligent Computer Mathematics, 7–12 Jul, Bath, UK; Deadline 8 Mar
  http://cicm-conference.org/2013/
→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  3–5 April 2013, Exeter, UK.  3 Hands-on Tutorials on Economics
  http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/

-- 
Christoph Lange, Universität Bremen (now: University of Birmingham)
http://kwarc.info/clange, Skype duke4701

→ SePublica Workshop @ ESWC 2013.  Montpellier, France, 26-30 May.
  Deadline 4 Mar; http://sepublica.mywikipaper.org
→ Intelligent Computer Mathematics, 7–12 Jul, Bath, UK; Deadline 8 Mar
  http://cicm-conference.org/2013/
→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  3–5 April 2013, Exeter, UK.  3 Hands-on Tutorials on Economics
  http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ SePublica Workshop @ ESWC 2013.  Montpellier, France, 26-30 May.
  Deadline 4 Mar; http://sepublica.mywikipaper.org
→ Intelligent Computer Mathematics, 7–12 Jul, Bath, UK; Deadline 8 Mar
  http://cicm-conference.org/2013/
→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  3–5 April 2013, Exeter, UK.  3 Hands-on Tutorials on Economics
  http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/