We analyze how contractibility affects contract design. A major concern when designing research agreements is that researchers may use their funding to subsidize other projects. We show that, when research activities are not contractible, an option contract is optimal. The financing firm obtains the option to terminate the agreement and, in case of termination, broad property rights. The threat of termination deters researchers from cross-subsidization, and the cost of exercising the termination option deters the financing firm from opportunistic termination. We test this prediction using 580 biotechnology research agreements. Contracts with termination options are more common when research is non-contractible.

Flavins are arguably one of the most versatile cofactors in biology, resulting from their ability to facilitate both 1e- and 2e- transfer reactions, as well as their widely-varying reduction potentials that can be tuned by the local protein environment. Flavins have three redox states: oxidized (OX), 1e--reduced semiquinone (SQ), and 2e--reduced hydroquinone (HQ). Their reactivity in redox processes is determined by E’OX/SQ and E’SQ/HQ, which is affected by electrostatic and H-bonding interactions in the flavin binding site. Free in solution, flavins exhibit “inverted potentials”, where the 1e– reduced state is more unstable than the fully-reduced state. The flavin binding site of flavodoxins, a class of electron transfer flavoproteins, alters the 1e- reduction potentials such that they become “normally” ordered, stabilizing E’OX/SQ relative to E’SQ/HQ. In other cases, the protein environment can increase potential inversion. A dramatic example can be found in flavin-based electron bifurcation (FBEB), which utilizes significant potential separation (ΔE) to conserve energy from exergonic redox reactions by concomitantly driving endergonic ET. The properties of the flavin binding site that induce this inversion are unknown, largely due to the limited mutagenesis space in authentic EB-ases and lack of physical methods for measuring highly-inverted 1e- reduction potentials. Since potential separation is fundamental to the mechanism of energy conservation in FBEB, understanding its cause is both interesting from a basic science perspective, and valuable to the field of electrocatalysis. To move towards this goal, it is essential to develop minimalist models for potential inversion, since the study of this phenomenon in native EB-ases is nontrivial. We have demonstrated that iLOV can be used as a model flavoprotein to evidence the effects of near-flavin mutations on redox behavior and potential inversion, substituting Lys to illustrate the influence of an ionizable and H-bonding functional group on semiquinone stability. We have designed expression and reconstitution methods to recombinantly produce iLOV WT, Q104K, and Q104A in high holoprotein yield. The 2e- reduction potential of iLOV WT and Q104K was measured by protein film voltammetry, and equilibration studies with a redox dye were conducted to confirm that protein-film electrochemistry corresponded to bulk properties. The semiquinone protonation state was characterized by EPR and UV-vis. Using spectral data to infer concentrations of the three flavin redox states at electrochemical equilibrium, ΔE was calculated for iLOV WT, iLOV Q104K and iLOV Q104A. The results suggest that iLOV WT has the most inverted 1e- potentials, followed by Q104A, with Q104K having the least potential separation. The substitution of Ala at the N5 position appeared to stabilize the SQ, although this is likely due to exposure to ambient light. The addition of Lys at N5 appears to influence the thermodynamic properties of the flavin such that E’OX/SQ, and seemingly E’SQ/HQ, is more positive. This can be rationalized by its relative acidity and closer pKa matching between the flavin and Lys, as compared to Gln in iLOV WT. Our discoveries on the crucial elements of potential inversion in flavin redox chemistry may shed light on the mechanisms of potential tuning in natural systems, particularly extreme potential inversion of EB-ases.

In the last twenty years, Italy has experienced an unprecedented influx of immigrants from non-European countries, which has posed challenges to its social, political, and cultural structures. In the tradition of Neorealist political engagement, Italian film directors have been among the first intellectuals to explore the issues that the increasing diversity of the Italian nation poses to Italians and foreign-born immigrants alike, beginning with Michele Placido’s Pummarò (1990) and Gianni Amelio’s Lamerica (1994). This article focuses on three more recent examples of Italian migration cinema: Marco Tullio Giordana’s Quando sei nato non puoi più nasconderti (2005), Vittorio De Seta’s Lettere dal Sahara (2004), and Mohsen Melliti’s Io, l’altro (2007). In each of these films, the Mediterranean is constructed as a transitional space of personal transformation, where identities are defined, alliances formed and conflicts played out. It is a privileged space of dialogue and encounter with the other, reasserting the relevance of “il suo statuto di confine, di interfaccia, di mediazione tra i popoli.” Through an analysis especially informed by Franco Cassano’s Pensiero meridiano, as well as Jacques Derrida’s notion of hospitality, and Slavoj Zizek’s understanding of liberal multiculturalism, the article shows how these films offer a critique of Italian societal practices and individual cultural attitudes towards otherness. The representation of the Mediterranean in these films, in particular, offers an opportunity to contemplate Europe’s own contingency, to experience and recognize the limits of its practices of hospitality toward immigrants. It is precisely this tension that which, according to Derrida, makes the perfectibility of laws and social practices, if not a political reality, at least a possibility.

Human computation and crowdsourcing have been successfully proposed and applied to solve problems that are difficult to solve due to either the limitations of current computing technology or the existence of only a few experts. A common way to solve problems through human computation and crowdsourcing systems is to convert them into interactive games that target a wide audience of non-experts. Leveraging humans’ innate ability to recognize patterns, a few systems have solved the problem of synthesizing loop invariants through single-player puzzle games.

This thesis proposes to apply human computation to synthesize loop invariants by having players find them through a multiplayer game. We explain the challenges involved in designing such games and explore the advantages multiplayer games offer over single-player games in terms of players’ efficiency of solving problems and the level of fun they have.

Parsers – programs that extract structure from strings – are fundamental components of many software systems. Although parsing theory may have found its roots in early work on programming languages, the growth of computing during the intervening decades has expanded the role of parsers into many systems one might not immediately expect: email clients, video games, spreadsheet programs, and relational databases are only a few among myriad examples of systems that extract structured information from input text. As a result, the construction of parsers has become a ubiquitous programming task that is performed by developers across a large spectrum of domains. It is not just a task for programming language experts anymore.

Unfortunately, despite over forty years of research on parsing, writing parsers remains a painstaking, manual process that is prone to subtle bugs and pitfalls. Existing tools for generating parsers assume a great deal of background knowledge in parsing and formal language theory, so the learning curve is high.

In this dissertation, we argue that it is possible to make parsing more accessible by combining interactive visual feedback with the programming-by-example paradigm, wherein users synthesize programs simply by providing example inputs and outputs demonstrating the result of the intended computation. Towards this aim, we present novel algorithms for (1) constructing syntactic specifications by example, (2) constructing lexical analyses by example, and (3) visualizing progress toward parser completion. We instantiate these algorithms in two graphical development environments we have implemented, Parsify and its successor Parsimony, whose central user interaction paradigm is that of programming-by-example. Finally, via user study we demonstrate that non-expert users indeed show significantly better performance when using our system.

Michigan State University

Due to their safety-critical nature, cyber-physical systems (CPS) demand the most rigorous verification techniques. However, the complexity of the domain puts many cyber-physical systems outside the scope of automated verification tools. Formal deductive proofs hold the potential to verify virtually any property of any system, but proofs for practical cyber-physical systems often require an impractical amount of manual effort. This proof burden can be mitigated by capturing common reasoning patterns in powerful higher-order proof rules. Existing work has focused on proof rules applicable to arbitrary hybrid systems (a formal model for CPS), but many systems actually fall into more constrained classes. One such class of systems are called sampled-data systems, in which a discrete controller runs periodically. In this dissertation, we complement general hybrid system proof rules with a series of rules that leverage the particular structure of sampled-data systems. We demonstrate the applicability of these rules on the double integrator, an important model in robotic and vehicle systems. All work is formalized in the Coq proof assistant, whose expressive logic is crucial to maintaining soundness while applying domain-specific proof rules for sampled-data systems. Finally, we experimentally evaluate our results by implementing verified controllers on a quadcopter and conducting flight tests.

Dependently-typed functional languages are increasingly popular, but due to the complexity of their type systems, there is still a lot of friction in the user experience, both for beginners who try to learn the concepts, and expert users who must write and maintain complex code bases. We explore ways to alleviate those burdens by providing novel front-end tooling for this class of languages.

In order to help beginners, we explore new visualizations and automation techniques, focusing on three pain points we identified in the learning process. We evaluate, via a longitudinal user study and an A-B study, their effectiveness in terms of learning to use those languages, enjoyment of the learning process, and productivity on solving beginner-level exercises.

In order to help experts, we prototype a tool that helps in the refactoring of programs, partially eliminating the tedium of propagating changes throughout large code bases. Our tool is built around a small dependently-typed functional core language, but it supports extensions to richer languages, with similar or weaker type systems. We demonstrate this by extending it to support OCaml, a widely used, modern functional language without dependent types.