Wed 17 Jun 2015 14:50 - 15:15 at PLDI Main RED (Portland 256) - Logic Chair(s): Nate Foster

The power of linear and affine logic lies in their ability to model state change. However, in a trustless, peer-to-peer setting, it is difficult to force principals to commit to state changes. We show how to solve the peer-to-peer affine commitment problem using a generalization of Bitcoin in which transactions deal in types rather than numbers. This has applications to proof-carrying authorization and mechanically executable contracts. Importantly, our system can be—and is— implemented on top of the existing Bitcoin network, so there is no need to recruit computing power to a new protocol.

Wed 17 Jun
Times are displayed in time zone: Tijuana, Baja California change

14:00 - 15:40
LogicResearch Papers at PLDI Main RED (Portland 256)
Chair(s): Nate FosterCornell University
14:00
25m
Talk
Automatic Induction Proofs of Data-Structures in Imperative Programs
Research Papers
Duc-Hiep ChuNational University of Singapore, Joxan JaffarNational University of Singapore, Minh-Thai TrinhNational University of Singapore
Media Attached
14:25
25m
Talk
Compositional Certified Resource Bounds
Research Papers
Quentin CarbonneauxYale University, Jan HoffmannYale University, Zhong ShaoYale University
Link to publication Media Attached
14:50
25m
Talk
Peer-to-peer Affine Commitment using Bitcoin
Research Papers
Karl CraryCarnegie Mellon University, Michael J. Sullivan
Media Attached
15:15
25m
Talk
Termination and Non-Termination Specification Inference
Research Papers
Ton Chanh LeNational University of Singapore, Shengchao QinTeesside University, Wei-Ngan ChinNational University of Singapore
Media Attached