Geometrisation of first-order logic

Dr. Roy Dyckhoff will give a talk titled, “Geometrisation of first-order logic”.

Abstract:

We show that every first-order theory T has a conservative extension G_T that is a geometric theory. Reasoning problems in T can therefore be replaced by problems in G_T, where the methods of geometric (aka ‘coherent’) logic are applicable. We discuss related work by Skolem (1920), Antonius (1975), Bezem and Coquand (2005), Fisher (2007–..), Polonsky (2011) and Mints (2012).

(A formula is **positive** iff built from atoms using \exists, \land and \lor. A **geometric implication** is the universal quantification of a formula C -> D where C and D are positive. A theory is **geometric** iff axiomatised by geometric implications. Lots of mathematical theories are geometric. Reasoning in a geometric theory usually avoids the unnatural conversions of resolution-based theorem proving, and produces intuitionistically sound proofs)

Joint work with Sara Negri (Helsinki).

Event details

  • When: 21st February 2014 12:00 - 13:00
  • Where: Maths 1A Tut Rm
  • Format: Talk

An Experience of Peer Instruction

Talk by Quintin Cutts, University of Glasgow

Fed up with talking at students in one-hour chunks? Fed up with them not turning up, or falling asleep, or not remembering anything you said? Alternatively, are you fed up going to seminars where you get talked at for 55 minutes with only 5 minutes to ask questions?

Come along on Tuesday for a taste of something different. Peer Instruction (PI) is a pedagogy from the “flipped classroom” stable, where students do preparatory work before coming to lecture, and the lecture itself is more of a tutorial with lots of small-group and class-wide discussion. PI has been documented to give “times two” learning gains on standardised tests over traditional methods. Students work hard in these lectures, making your and their time worthwhile – one student said this term “I felt mentally tired after these lectures, which felt really good actually!”

I’ll run the first part of the session (at least) as if we were in a PI classroom. This will only really work if you have already at least skim-read the short three page article linked below which introduces some of the aspects of PI – saving me having to go over it again in the seminar, and allowing you to process it and be ready to grill me in the session itself!

http://dl.acm.org/citation.cfm?doid=2076450.2076459

Event details

  • When: 17th December 2013 14:00 - 15:00
  • Where: Cole 1.33a
  • Format: Talk

Enterprise First: How to Start a Tech Startup

Enterprise First is the UK’s top graduate startup accelerator, sponsored by government as well as global companies such as McKinsey, KPMG and Microsoft.
 Please see the event description below and check out the facebook event at https://www.facebook.com/events/451961804910008

 

How to Start a Tech Startup

Entrepreneur First is coming to St Andrews to deliver an intensive, practical workshop on how to actually start a startup as a computer scientist.
 
When: Friday 22nd November, 4-5pm.
Where: Physics Theatre C
Why: Maybe you’ve already thought of founding a startup after graduation. But, maybe you’re going into a tech company to gain experience or staying in academia to research your idea. Entrepreneur First thinks best way to build something amazing is to actually do it from Day 1. Why should you compromise? Last year 32 graduates joined Entrepreneur First and built 11 companies now worth over $35million, two of which went on to Y Combinator. Come and find out how.
 
This is the hardest, most challenging career path available, and is almost exclusively open to technical graduates. The Founders of Entrepreneur First will show you what it takes, and highlight previous St Andrews students who have gone on to create successful startups on the programme.
 
If you’re the sort of person who wants to build big, world-changing products, Entrepreneur First was designed for you. Almost everyone has strong technical backgrounds. Entrepreneur First is the only programme in the world to select individuals purely on the basis of talent, often pre idea and pre team, and give them the opportunity to build their ideas with other exceptional people.
 
Entrepreneur First is a not-for-profit backed by the City of London, McKinsey & Company, KPMG, Microsoft, Nokia, Experian, Osborne Clarke, Rackspace, Sky, SVB, and Workspace. You can read about them in the BBC, The Daily Telegraph, The Wall Street Journal, The Guardian, Tech City News, and the Financial Times. Find out more:

Event details

  • When: 22nd November 2013 16:00 - 17:00
  • Where: Phys Theatre C
  • Format: Talk

Talk by Susmit Sarkar

Title: “Shared-Memory Concurrency in the Real World: Working with Relaxed Memory Consistency”

Abstract:

Shared-memory concurrency is now mainstream, from phones to servers. However, real-world implementations do not validate the basic assumption of Sequential Consistency traditionally made in work on concurrent programming and verification. Instead, we get subtle relaxed consistency models. Furthermore, the consistency models of different hardware architectures vary widely and have often been poorly defined, while programming language models (aiming to abstract from hardware details) are different again.

This talk is about what relaxed consistency models we actually get on current mainstream systems: the x86 multiprocessor architecture, the IBM Power and ARM lines of multiprocessors, and in the new concurrency model in ISO C/C++11. Part of the challenge here is that neither hardware microarchitects nor low-level programmers (for operating systems or compilers) know exactly what you get, or what you should get. I will discuss the models that are getting some agreement/acceptance, and how we can use those models.

Event details

  • When: 4th April 2013 12:00 - 13:00
  • Where: Cole 1.04
  • Format: Talk

Talk by Dr Jost Berthold Thursday 14th March

Thursday 14th March, the regular meeting of the Functional Programming group will give the floor to our guest Dr. Jost Berthold for a public talk called “High-Level Parallel Computing in Finance — Haskell Case Studies within HIPERFIT –” .

The presentation will take place from 12.00 to 13.00, in the Jack Cole building, room 1.04 (upstairs), and everyone is welcome.

If you intend to come to the talk, it would be helpful (but is not essential) to drop me (fs39) a one-line email beforehand, to be sure that the reserved room has a suitable size.

Abstract: Continue reading

Event details

  • When: 14th March 2013 12:00 - 13:00
  • Where: Cole Bldg
  • Format: Seminar, Talk

Computer Gaming Industry careers: Aardvark Swift presentation – Get in the Game

Tuesday 27 November, 1400-1500, 1.33a Jack Cole building (Computer Science)

Aardvark Swift, recruitment agents for the gaming industry, will be talking about how to break into the sector. Get advice from those in the know on the key skills you will need, the common pitfalls, and how to maximise your chances. Ideal for programming enthusiasts of all disciplines, and for anyone interested in a gaming career. http://www.aswift.com/index.jsp#holder1-start

AS will also be giving details of how to enter their nationwide programming competition Search for a Star! SFAS is designed to highlight and reward the UK’s most promising video games developers. The winner will be announced at the Eurogamer 2013, with last years winner securing a job at Sony Evolution . This years competition is being sponsored by Microsoft http://www.aswift.com/searchforastar/

Event details

  • When: 27th November 2012 14:00 - 15:00
  • Where: Cole 1.33a
  • Format: Talk

Forthcoming talk by SICSA Distinguished Visitor

Room 1.33a at 2:00 pm on Friday 7th September 2012

  • Introduction to Grammatical Formalisms for Natural Language Parsing
  • Giorgio Satta, Department of Information Engineering, University of Padua, Italy

Abstract:
In the field of natural language parsing, the syntax of natural languages is

modeled by means of formal grammars and automata. Sometimes these formalisms

are borrowed from the field of formal language theory and are adapted to the
task at hand, as in the case of context-free grammars and their lexicalized
versions, where each individual rule is specialized for one or more lexical
items. Sometimes these formalisms are newly developed, as in the case of
dependency grammars and tree adjoining grammars. In this talk, I will
briefly overview several of these models, discussing their mathematical
properties and their use in parsing of natural language.

Event details

  • When: 7th September 2012 14:00 - 15:00
  • Where: Cole 1.33a
  • Format: Seminar, Talk

TayViz – The bi-monthly meeting of the Tayside and Fife network for data visualisation

Talks:

Information Visualization Research in the SACHI group

Speaker: Aaron Quigley

Abstract:

Aaron will provide a quick overview of the incipient InfoViz research and prospects of the SACHI group.

A few examples of visualisation in computational systems biology of anti-inflammatory and anticancer drug actions

Speaker: Alexey Goltsov

Abstract:

Visualization is a key aspect in computational systems biology to analyse results of in silico modelling, generate and test hypothesises.  Some examples of visualisation in computational systems biology of cellular response to drug intervention are discussed. First, the developed method of the complex dynamics visualisation of enzyme kinetics is discussed and illustrated with the dynamic visualisation of cyclooxygenase enzyme function and its inhibition by anti-inflammatory drug, aspirin. Second, 3D dynamic visualisation of thrombosis in blood vessel is demonstrated based on the developed agent-based model of blood clotting and anticoagulation drug effect. Third, visualisation in computational systems biology of cancer are discussed and illustrated with the visualisation methods of the determination of promising drug targets and analysis of changing sensitivity of tumor to anticancer therapy at different oncogenic mutations.

FatFonts: Combining the Symbolic and Visual Aspects of Numbers

Speaker: Miguel Nacenta

Abstract:

In this talk I present a new technique for visualisation that makes use of typography. FatFonts is a technique for visualizing quantitative data that bridges the gap betweennumeric and visual representations. FatFonts are based onArabic numerals but, unlike regular numeric typefaces, theamount of ink (dark pixels) used for each digit is propor-tional to its quantitative value. This enables accurate read-ing of the numerical data while preserving an overall visual context. During the talk, I discuss the challenges of this approach, it’s possible uses, and how to use it in visualizations.

Bio:

Miguel Nacenta is a Lecturer in the School of Computer Science. He is interested in new interaction form factors (e.g., tabletops, multi-touch, multi-display environments), perception, and information visualisation.

Event details

  • When: 15th May 2012 18:30 - 20:30
  • Where: Cole 1.33a
  • Format: Talk

Security and Privacy in mHealth systems

Mobile computing and sensing technologies present exciting opportunities for healthcare. Wireless sensors worn by patients can automatically deliver medical
sensor data to care providers, family members, or other caregivers, providing new opportunities to diagnose, monitor, and manage a wide range of medical
conditions. Using the mobile phones that patients already carry to provide connectivity between sensors and providers can help to keep costs low and
deployments simple. However, there are many security and privacy challenges involved in developing a system that will protect the patient’s privacy and the
integrity of the data collected. In this talk I describe the advent of these “mHealth” systems, survey the security and privacy issues, and describe research
underway at Dartmouth to address these challenges.

Biography

David Kotz is the Champion International Professor, in the Department of Computer Science, and Associate Dean of the Faculty for the Sciences, at Dartmouth
College in Hanover NH. During the 2008-09 academic year he was a Visiting Professor at the Indian Institute of Science, in Bangalore India, and a Fulbright
Research Scholar to India. At Dartmouth, he was the Executive Director of the Institute for Security Technology Studies from 2004-07. His research interests
include security and privacy, pervasive computing for healthcare, and wireless networks. He has published over 100 refereed journal and conference papers. He
is an IEEE Fellow, a Senior Member of the ACM, a member of the USENIX Association, and a member of Phi Beta Kappa.
After receiving his A.B. in Computer Science and Physics from Dartmouth in 1986, he completed his Ph.D in Computer Science from Duke University in 1991 and
returned to Dartmouth to join the faculty. For more information see http://www.cs.dartmouth.edu/~dfk/.

Event details

  • When: 22nd August 2011 11:30 - 12:30
  • Where: Cole 1.33a
  • Format: Seminar, Talk

The use of regret and forgiveness

Dr Steve Marsh.

Regret, the emotion arising from counterfactual reasoning about action
and inaction, is a powerful tool in the arsenal of trust-reasoning and
enabling technologies. One aspect of the tool, Regret Management, is the
enforcement of a view of System Trust in technological approaches in
order to preserve and encourage respect for concerns such as data
protection, privacy, and cyber-social interaction. Forgiveness, as a
tool in the broad spectrum of computational trust, helps agents reason
about and rebuild relationships that may have been damaged by some
action, and is particularly useful in areas where, as online, cheap
pseudonyms can exist. This talk will examine regret and forgiveness from
the point of view of agents or devices in connected environments, where
humans are present actors, and show how enforcement of regret management
and forgiveness measures may be efficacious.

Steve Marsh is a Research Scientist in the Network Security Group at in
the Communications Research Centre in Ottawa, Ontario, Canada.

His PhD (University of Stirling, 1994) was a seminal work that
introduced the first formalisation of the phenomenon of trust (the
concept of ‘Computational Trust’), and applied it to Multi Agent
Systems. As a milestone in trust research, it brought together disparate
disciplines and attempted to make sense of a vital phenomenon in human
and artificial societies, and is still widely referenced today. Steve’s
current work builds extensively on this model, applying it to network
security, MANETs, and mobile device security.

His research interests include computational trust, trust management,
regret and regret management, and socially adept technologies. He is the
Canadian delegate to IFIP Technical Committee 11: Security and Privacy
Protection in Information Processing Systems. He is an adjunct professor
at UNB (Computer Science), UOIT (Business and IT) and Carleton
University (Systems and Computer Engineering and Cognitive Science).

Event details

  • When: 26th July 2011 14:00 - 15:00
  • Where: Cole 1.33a
  • Format: Talk