- When: 30th November 2017 12:00 - 13:00
- Where: Cole 1.33b
- Format: Talk
Type systems are often presented in a declarative style, but with an emphasis on ensuring that there is some sort of type synthesis algorithm. Since Pierce and Turner’s “Local Type Inference” system, however, there has been a small but growing alternative: bidirectional typing, where types are synthesized for variables and elimination forms, but must always be proposed in advance for introduction forms and checked. You can still get away without any type annotations, as long as you write only normal forms. But where’s the fun in that? If you want to write terms that compute, you need to write type annotations at exactly the point where an introduction form collides with its elimination form, showing exactly the type at which computation is happening.
For type systems with some sorts of value dependency, the bidirectional approach seriously cuts down on the amount of annotation required in terms, needed only to achieve type synthesis. We have a real opportunity to reduce clutter and also to give a clearer account of the connections between types and computation.
But it doesn’t stop there. A disciplined approach to the construction of bidirectional type systems makes it easier to get their metatheory right. I’ll show this by reconstructing Martin-Löf’s 1971 type theory (the inconsistent one) in a bidirectional style and show why it has type
preservation, even without normalization.
Dependent types are increasingly used in functional programming languages. The surface syntax of dependent types, as seen by a programmer, is elaborated by a compiler into an internal, type-theoretic representation. In order to perform this step, the compiler needs to infer a nontrivial amount of information to successfully type-check the internal representation. This process—type refinement—is complex, implementation dependent, and very few formal developments currently exist. We discuss a novel and simpler formalisation of type refinement in first order type theory with dependent types. We propose a translation of type-refinement problems to Horn-Clause logic with explicit proof-terms, using proof-relevant resolution as the type inference mechanism.
Adam Barwell (adb23) will be presenting a summary of his recently submitted thesis.
Software Defined Networking (SDN) or Virtual Networks (VNs) are required for cloud tenants to leverage demands. However, multi-tenancy can be compromised without proper isolation. Much research has been conducted into VN Isolation; many researchers are not tackling security aspects or checking if their isolation evaluation is complete. Therefore, data leakage is a major security concern in the cloud in general.
This research uses an OpenStack VN and OpenStack Tenant Network to test multi-tenancy features. We are evaluating the relationship between isolation methods used in cloud VN and the amount of data being leaked through using penetration tests. These tests will be used to identify the vulnerabilities causing cloud VN data leakage and to investigate how the vulnerabilities, and the leaked data, can compromise the tenant Virtual Networks.
Computational methods are having a considerable influence on contemporary neuroscience research: in data collection (non-invasive functional brain imaging), data analysis and computational modelling of healthy and abnormal brain and behaviour. The presentation is in two parts. Part 1 is an overview of the current main computational-neuroscience areas in research. Part 2 focuses on some recent high impact research into potential empirical and mechanistic biomarkers for psychiatric disorders.
Speaker: Jan de Muijnck-Hughes
Communicating protocols are a cornerstone of modern system design.
However, there is a disconnect between the different tooling used to design, implement and reason about these protocols and their implementations.
Session Types are a typing discipline that help resolve this difference by allowing protocol specifications to be used during type-checking to ensure that implementations adhere to a given specification.
Idris is a general purpose programming language that supports full-dependent types, providing programmers with the ability to reason more precisely about programs.
This talk introduces =Sessions=, our implementation of Session Types in Idris, and demonstrates =Sessions= ability to design and realise several common protocols.
=Sessions= improves upon existing Session Type implementations by introducing value dependencies between messages and fine-grained channel management during protocol design and implementation.
We also use Idris’ support for EDSL construction to allow for protocols to be designed and reasoned about in the same language as their implementation.
Thereby allowing for an intrinsic bond to be introduced between a protocol’s implementation and specification, and also with its verification.
Using =Sessions=, we can reduce the existing disconnect between the tooling used for protocol design, implementation, and verification.
The increasing importance of parallelism has motivated the creation of better abstractions for writing parallel software, including structured parallelism using nested algorithmic skeletons. Such approaches provide high-level abstractions that avoid common problems, such as race conditions, and often allow strong cost models to be defined. However, choosing a combination of algorithmic skeletons that yields good parallel speedups for a program on some specific parallel architecture remains a difficult task. In order to achieve this, it is necessary to simultaneously reason both about the costs of different parallel structures and about the semantic equivalences between them. This paper presents a new type-based mechanism that enables strong static reasoning about these properties. We exploit well-known properties of a very general recursion pattern, hylomorphisms, and give a denotational semantics for structured parallel processes in terms of these hylomorphisms. Using our approach, it is possible to determine formally whether it is possible to introduce a desired parallel structure into a program without altering its functional behaviour, and also to choose a version of that parallel structure that minimises some given cost model.
GPS has enabled a number of location based services outdoors, but the problem of localisation remains open in GPS-denied environments, such as indoors and underground. In this talk, I will discuss the key challenges to accurate and robust position estimation, and will describe a variety of sensor modalities and algorithms developed at Oxford to address this problem.
The talk will cover inertial, radio-based and vision-based localisation approaches and their advantages and disadvantages in different settings.
Niki Trigoni is a Professor at the Oxford University Department of Computer Science and a fellow of Kellogg College. She obtained her PhD at the University of Cambridge (2001), became a postdoctoral researcher at Cornell University (2002-2004), and a Lecturer at Birkbeck College (2004-2007). Since she moved to Oxford in 2007, she established the Sensor Networks Group, and has conducted research in communication, localization and in-network processing algorithms for sensor networks. Her recent and ongoing projects span a wide variety of sensor networks applications, including indoor/underground localization, wildlife sensing, road traffic monitoring, autonomous (aerial and ground) vehicles, and sensor networks for industrial processes.
Quicksort is a well-known sorting algorithm used to implement sort functionality in many libraries. The presentation isn’t really about the algorithm itself but rather about how to actually create an efficient implementation of the algorithm: a text-book implementation of the algorithm actually is not that quick (even if the pivot is chosen cleverly). It takes paying some attention to detail to improve the implementation significantly. This presentation starts with a simple implementation and makes incremental improvements to eventually yield a proper generic and fast sorting function. All code will be in C++ but it should be possible to follow the majority of the reasoning with knowledge of another programming language.
Dietmar Kühl is a senior software developer at Bloomberg L.P. working on the data distribution environment used both internally and by enterprise installations at clients. Before joining Bloomberg he has done mainly consulting for software projects in the finance area. He is a regular attendee of the ANSI/ISO C++ standards committee, presents at conferences, and he used to be a moderator of the newsgroup comp.lang.c++.moderated. He frequently answers questions on Stackoverflow.