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 JunDisplayed time zone: Tijuana, Baja California change
Wed 17 Jun
Displayed time zone: Tijuana, Baja California change
14:00 - 15:40 | |||
14:00 25mTalk | Automatic Induction Proofs of Data-Structures in Imperative Programs Research Papers Duc-Hiep Chu National University of Singapore, Joxan Jaffar National University of Singapore, Minh-Thai Trinh National University of Singapore Media Attached | ||
14:25 25mTalk | Compositional Certified Resource Bounds Research Papers Link to publication Media Attached | ||
14:50 25mTalk | Peer-to-peer Affine Commitment using Bitcoin Research Papers Media Attached | ||
15:15 25mTalk | Termination and Non-Termination Specification Inference Research Papers Ton Chanh Le National University of Singapore, Shengchao Qin Teesside University, Wei-Ngan Chin National University of Singapore Media Attached |