Skip to main content
Home

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Manifest Sharing with Session Types

Series
International Conference on Functional Programming 2017
Embed
Stephanie Balzer (Carnegie Mellon University, USA) gives the third talk in the third panel, Contracts and Sessions, on the 3rd day of the ICFP conference.
Co-written Frank Pfenning (Carnegie Mellon University, USA).

Session-typed languages building on the Curry-Howard isomorphism between linear logic and session-typed communication guarantee session fidelity and deadlock freedom. Unfortunately, these strong guarantees exclude many naturally occurring programming patterns pertaining to shared resources. In this paper, we introduce sharing into a session-typed language where types are stratified into linear and shared layers with modal operators connecting the layers. The resulting language retains session fidelity but not the absence of deadlocks, which can arise from contention for shared processes. We illustrate our language on various examples, such as the dining philosophers problem, and provide a translation of the untyped asynchronous pi-calculus into our language.
Creative Commons Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK (BY-NC-SA): England & Wales; https://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Stephanie Balzer
Keywords
computing
programming
technology
Department: Department of Computer Science
Date Added: 22/01/2018
Duration: 00:21:08

Subscribe

Download

Whip: Higher-Order Contracts for Modern Services

Series
International Conference on Functional Programming 2017
Embed
Lucas Waye (Harvard University, USA), gives the second talk in the third panel, Contracts and Sessions , on the 3rd day of the ICFP conference.
Co-written by Christos Dimoulas (Harvard University, USA), Stephen Chong (Harvard University, USA).

Modern service-oriented applications forgo semantically rich protocols and middleware when composing services. Instead, they embrace the loosely-coupled development and deployment of services that communicate via simple network protocols. Even though these applications do expose interfaces that are higher-order in spirit, the simplicity of the network protocols forces them to rely on brittle low-level encodings. To bridge the apparent semantic gap, programmers introduce ad-hoc and error-prone defensive code. Inspired by Design by Contract, we choose a different route to bridge this gap. We introduce Whip, a contract system for modern services. Whip (i) provides programmers with a higher-order contract language tailored to the needs of modern services; and (ii) monitors services at run time to detect services that do not live up to their advertised interfaces. Contract monitoring is local to a service. Services are treated as black boxes, allowing heterogeneous implementation languages without modification to services' code. Thus, Whip does not disturb the loosely coupled nature of modern services.
Creative Commons Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK (BY-NC-SA): England & Wales; https://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Lucas Waye
Keywords
technology
engineering
programming
Department: Department of Computer Science
Date Added: 22/01/2018
Duration: 00:18:17

Subscribe

Download

The Role of Deterrence in Managing Great Power Competition

Series
Changing Character of War
Embed
This seminar will not only offer a core foundation in the concept of deterrence, from a practitioner's perspective, but explore its utility and application to present day conflict scenarios in Europe, in particular the case of Russia and NATO.

In the United States national security and policy discourse has notably shifted away from low intensity conflict and back to the threat from peer and near-peer competitors. With great power competition and confrontation back at the center of policy discussions, there is a revived interest in the subject of conventional and nuclear deterrence, along with managing alliance politics. While interest in the subject of deterrence and compellence has risen sharply, after decades of counter insurgency and stability operations against adversaries with no escalation dynamics, knowledge of the subject is at an all time institutional low in modern day military establishments.

Mr. Michael Kofman is a Senior Research Scientist at CNA Corporation and a Fellow at the Kennan Institute, Woodrow Wilson International Center in Washington, D.C. Mr. Kofman directs the Russia Studies Program at CNA, where he specializes in the Russian armed forces and security issues in the former Soviet Union. Mr. Kofman's other affiliations include a fellowship at the Modern War Institute at West Point, and as a Senior Editor on War on the Rocks.

Episode Information

Series
Changing Character of War
People
Michael Kofman
Keywords
deterrence; nuclear; politics
Department: Pembroke College
Date Added: 22/01/2018
Duration:

Subscribe

Download

Lincoln Leads in Medicine

Series
Lincoln College
Embed
Lincoln's medical breakthroughs: The past, present and future.
Lincoln has a history of pioneering medical research, particularly in relation to developing penicillin and researching cell biology. In this Lincoln Leads session, Dr Eric Sidebottom (an authority on Oxford's medical history and former student of Lord Florey) takes us on a journey back in time to chart Lincoln's longstanding connection with the Dunn School and to take a closer look at some of the most famous Lincoln scientists - from John Radcliffe to Howard Florey and Norman Heatley. Returning to the present day, Professor David Vaux discusses his current research, which focuses on the nuclear envelope and its associated disease states. The nuclear envelope is the barrier between the nucleus and the rest of the cell, and his team study the roads and tunnels that carry molecules deep into or through the nucleus. If that wasn’t enough, the other team in his lab study how diseases such as Alzheimer’s, diabetes, and motor neuron disease work on the cellular level. Finally, after nearly a century of pathology-slanted studies, the Dunn School has begun turning its face to modern cell biology. Mustafa Aydogan will be addressing the present and future of this transition through the lens of his observations at the Dunn School, as well as the type of research he does in the laboratory on a daily basis.

Episode Information

Series
Lincoln College
People
Eric Sidebottom
David Vaux
Mustafa Aydogan
Francesca Donnellan
Keywords
Lincoln College
lincoln leads
Medicine
history
immunology
penicillin
Department: Lincoln College
Date Added: 22/01/2018
Duration: 00:57:12

Subscribe

Download

The Future of Healthcare - Evidencer and Value Based

Series
Evidence-Based Health Care
Embed
Muir Gray is now working with both NHS England and Public Health England to bring about a transformation of care with the aim of increasing value for both populations and individuals. Here he gives a talk on improving healthcare systems.

Here are some questions we cannot answer after nearly 70 years of a purportedly National Health Service. The lecture will address these questions and how they can be answered.
1. Is the service for people with seizures and epilepsy in Manchester of higher value than the service in Liverpool?
2. How many liver disease services are there in England and how many should there be?
3. Which service for people at the end of life in London provides the best value?
4. Is the service for people with asthma of higher than the service in Somerset?
5. How many services are there for people with MusculoSkeletal Disease in the North East, and which gives best value?
We cannot answer them because we deliver care that is institutionally based not population based but to do so will need new knowledge and skills to answer questions such as:
1. What do you understand by the term complexity?
2. What is meant by the term system and how does it differ from a network?
3. What is meant by population based healthcare rather than bureaucracy based care?
4. What are the three meanings of the term value in 21st Century healthcare? Not ‘values’ as in 'we value diversity' but the economic meanings
5. What is the relationship between value and efficiency?
6. What is meant by the optimal use of resources?
7. What is meant by the term quality and how does it relate to value?
8. What is a system and a standard?
9. How would you assess the culture of an organisation?
10. How would you decide if an organisation had a strong culture of stewardship?

Muir Gray is now working with both NHS England and Public Health England to bring about a transformation of care with the aim of increasing value for both populations and individuals and published a series of How To Handbooks for example, How to Get Better Value Healthcare, How To Build Healthcare Systems and How To Create the Right Healthcare Culture.
His hobby is ageing and how to cope with it and he has published a book for people aged seventy called Sod 70! and one for the younger decade called Sod 60! This with Dr Claire Parker, and his book for people aged 40-60, titled Midlife, appeared in January 2017. Other books in the series on Sod Ageing are Sod it, Eat Well, with Anita Bean and Sod Sitting, Get Moving with Diana Moran, the Green Goddess. For people of all ages Dr Gray’s Walking Cure summarises the evidence on this wonderful means of feeling well, reducing the risk of disease and minimising disability should disease strike.
This talk was held as part of the Practice of Evidence-Based Health Care course which is part of the Evidence-Based Health Care Programme.

Episode Information

Series
Evidence-Based Health Care
People
Muir Gray
Keywords
EMB
Evidence-Based Medicine
Primary Care
Health Sciences
EBHC
Evidence-Based Health Care
Department: Medical Sciences Division
Date Added: 19/01/2018
Duration:

Subscribe

Download

Is it true? Why questions about the news are changing

Series
Reuters Institute for the Study of Journalism
Embed
Liz Corbin, editor, BBC Reality Check, gives a talk for the Business and Practice of Journalism Seminar Series.
Creative Commons Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK (BY-NC-SA): England & Wales; https://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
Reuters Institute for the Study of Journalism
People
Liz Corbin
Keywords
politics
truth
fact checking
fake news
bbc
Department: Department of Politics and International Relations (DPIR)
Date Added: 19/01/2018
Duration: 00:33:17

Subscribe

Download

A Metaprogramming Framework for Formal Verification

Series
International Conference on Functional Programming 2017
Embed
Sebastian Ullrich (KIT, Germany), gives the fourth talk in the second panel, Dependently Typed Programming, on the 3rd day of the ICFP conference.
Co-written by Gabriel Exner (Vienna University of Technology, Austria), Jared Roesch (University of Washington, USA), Jeremy Avigad (Carnegie Mellon University, USA), Leonardo De Moura (Microsoft Research).

Dependent type theory is a powerful framework for interactive theorem proving and automated reasoning, allowing us to encode mathematical objects, data type specifications, assertions, proofs, and programs, all in the same language.

Here we show that dependent type theory can also serve as its own metaprogramming language, that is, a language in which one can write programs that assist in the construction and manipulation of terms in dependent type theory itself. Specifically, we describe the metaprogramming language currently in use in the Lean theorem prover, which extends Lean's object language with an API for accessing natively implemented procedures and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our language is performant, and that it provides a convenient and flexible way of writing not only small-scale interactive tactics, but also more substantial kinds of automation.
Creative Commons Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK (BY-NC-SA): England & Wales; https://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Sebastian Ullrich
Keywords
technology
programming
computing
Department: Department of Computer Science
Date Added: 17/01/2018
Duration: 00:16:35

Subscribe

Download

Normalization by Evaluation for Sized Dependent Types

Series
International Conference on Functional Programming 2017
Embed
Andreas Abel (University of Gothenburg, Sweden), gives the first talk in the second panel, Dependently Typed Programming, on the 3rd day of the ICFP conference.
Co-written by Andrea Vezzosi (Chalmers University of Technology, Sweden), Theo Winterhalter (ENS Paris-Saclay, France).

Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional programs, the termination checker is an integral component of the trusted core, as validity of proofs depend on termination. However, a rigorous integration of full-fledged sized types into dependent type theory is lacking so far. Such an integration is non-trivial, as explicit sizes in proof terms might get in the way of equality checking, making terms appear distinct that should have the same semantics.

In this article, we integrate dependent types and sized types with higher-rank size polymorphism, which is essential for generic programming and abstraction. We introduce a size quantifier 'forall' which lets us ignore sizes in terms for equality checking, alongside with a second quantifier 'Pi' for abstracting over sizes that do affect the semantics of types and terms. Judgmental equality is decided by an adaptation of normalization-by-evaluation for our new type theory, which features type-shape-directed reflection and reification. It follows that subtyping and type checking of normal forms are decidable as well, the latter by a bidirectional algorithm.
Creative Commons Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK (BY-NC-SA): England & Wales; https://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Andreas Abel
Keywords
technology
programming
computing
Department: Department of Computer Science
Date Added: 17/01/2018
Duration: 00:20:21

Subscribe

Download

A Specification for Dependent Types in Haskell

Series
International Conference on Functional Programming 2017
Embed
Antoine Vizard (University of Pennsylvania, USA), gives the first talk in the second panel, Dependently Typed Programming, on the 3rd day of the ICFP conference.
Co-written by Stephanie Weiricc (University of Pennsylvania, USA), Pedro Henrique Azevedo de Amorim (Ecole Polytechnique, University of Campinas, Brazil), Richard A. Eisenberg( Bryn Mawr College, USA).

We propose a core semantics for Dependent Haskell, an extension of Haskell with full-spectrum dependent types. Our semantics consists of two related languages. The first is a Curry-style dependently-typed language with nontermination, irrelevant arguments, and equality abstraction. The second, inspired by the Glasgow Haskell Compiler's core language FC, is its explicitly-typed analogue, suitable for implementation in GHC. All of our results--chiefly, type safety, along with theorems that relate these two languages--have been formalized using the Coq proof assistant. Because our work is backwards compatible with Haskell, our type safety proof holds in the presence of nonterminating computation. However, unlike other full-spectrum dependently-typed languages, such as Coq, Agda or Idris, because of this nontermination, Haskell's term language does not correspond to a consistent logic.
Creative Commons Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK (BY-NC-SA): England & Wales; https://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Antoine Vizard
Keywords
computing
technology
reprogramming
Department: Department of Computer Science
Date Added: 17/01/2018
Duration: 00:18:51

Subscribe

Download

Herbarium Racketensis: A Stroll through the Woods (Functional Pearl)

Series
International Conference on Functional Programming 2017
Embed
Robby Findler (Northwestern University, USA), gives the first talk in the first panel, Domain-Specific Languages, on the 3rd day of the ICFP conference.
Co-written by Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, Northwestern University.

Domain-specific languages are the ultimate abstraction, dixit Paul Hudak. But what abstraction should we use to build such ultimate abstractions? What is sauce for the goose is sauce for the gander: a language, of course!

Racket is the ultimate abstraction-abstraction, a platform for quickly and easily building new ultimate abstractions. This pearl demonstrates Racket's power by taking a leisurely walk through the implementation of a DSL for Lindenmayer systems, the computational model par excellence of theoretical botany.
Creative Commons Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK (BY-NC-SA): England & Wales; https://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Robby Findler
Keywords
programming
technology
computing
Department: Department of Computer Science
Date Added: 17/01/2018
Duration: 00:20:08

Subscribe

Download

Pagination

  • First page
  • Previous page
  • …
  • Page 1794
  • Page 1795
  • Page 1796
  • Page 1797
  • Page 1798
  • Page 1799
  • Page 1800
  • Page 1801
  • Page 1802
  • …
  • Next page
  • Last page

Footer

  • About
  • Accessibility
  • Contribute
  • Copyright
  • Contact
  • Privacy
  • Login
'Oxford Podcasts' X Account @oxfordpodcasts | Upcoming Talks in Oxford | © 2011-2026 The University of Oxford