はてなブックマーク

The Weird World of Bi-Directional Programming Benjamin C. Pierce Microsoft Research, Cambridge (on leave from University of Pennsylvania) March, 2006 The View Update Problem I We apply a function to transform source to target S T The View Update Problem I We apply a function to transform source to target I Someone updates target S T Updated T update The View Update Problem I We apply a function to

The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software. The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Coq proof assistant. The exposition is intended for a broad range of readers, fro

Recent Activities John Hughes, Rini Bannerjee, and Benjamin C. Pierce. Adventures in Specification-Based Testing, October 2024. Invited talk at Isaac Newton Institute Workshop on Big Specification: Specification, Proof, and Testing at Scale. [ bib | slides ] Harrison Goldstein, Jeffrey Tao, Zac Hatfield-Dodds, Benjamin C. Pierce, and Andrew Head. Tyche: Making Sense of PBT Effectiveness. In Procee

In September, 2004, I posted a query to the Types list asking people to name the five most important papers ever written in the area of programming languages. This page collects the responses I received. (A few are missing because I am still tracking down bibliographic information.) Many thanks to Frank Atanassow, David Benson, Nick Benton, Karl Crary, Olivier Danvy, Mariangiola Dezani, Dan Friedm

Directory Index Name arith bot equirec fomega fomsub fullequirec fullerror fullfomsub fullfsub fullisorec fullomega fullpoly fullrecon fullref fullsimple fullsub fulluntyped fullupdate letexercise purefsub rcdsubbot recon reconbase simplebool tyarith untyped arith.tar.gz bot.tar.gz equirec.tar.gz fomega.tar.gz fomsub.tar.gz fullequirec.tar.gz fullerror.tar.gz fullfomsub.tar.gz fullfsub.tar.gz full

Information Coordinates, telephone numbers, schedule, and office hours Capsule bio Research Recent publications and talks All papers and software Current/Recent Projects: Property-based testing VERSE: A unified environment for testing, SML-based, and Rocq-based development of verified C code Unison: A robust, portable file synchronizer Books: Software Foundations series Types and Programming Langu

Note: The Unison project is now hosted on GitHub (here's a link). This web site is archival. Unison is a file-synchronization tool for OSX, Unix, and Windows. It allows two replicas of a collection of files and directories to be stored on different hosts (or different disks on the same host), modified separately, and then brought up to date by propagating the changes in each replica to the other.