Equational Reasoning about Object-Oriented Programs

Formal verification of software can be an enormous task. This fact brought some software engineers to claim that formal verification is not feasible in practice. One possible method of supporting the verification process is a programming language that provides powerful abstraction mechanisms combined with intensive reuse of code. In this thesis we present a strongly typed functional object-oriented programming language. This language features type operators of arbitrary kind corresponding to so-called type protocols. Sub classing and inheritance is based on higher-order matching, i.e., utilizes type protocols as basic tool for reuse of code. We define the operational and axiomatic semantics of this language formally. The latter is the basis of the interactive proof assistant VOOP (Verified Object-Oriented Programs) that allows the user to prove equational properties of programs interactively.

Improving Short DNA Sequence Alignment with Parallel Computing

Variations in different types of genomes have been found to be responsible for a large degree of physical diversity such as appearance and susceptibility to disease. Identification of genomic variations is difficult and can be facilitated through computational analysis of DNA sequences. Newly available technologies are able to sequence billions of DNA base pairs relatively quickly. These sequences can be used to identify variations within their specific genome but must be mapped to a reference sequence first. In order to align these sequences to a reference sequence, we require mapping algorithms that make use of approximate string matching and string indexing methods. To date, few mapping algorithms have been tailored to handle the massive amounts of output generated by newly available sequencing technologies. In otrder to handle this large amount of data, we modified the popular mapping software BWA to run in parallel using OpenMPI. Parallel BWA matches the efficiency of multithreaded BWA functions while providing efficient parallelism for BWA functions that do not currently support multithreading. Parallel BWA shows significant wall time speedup in comparison to multithreaded BWA on high-performance computing clusters, and will thus facilitate the analysis of genome sequencing data.

Effects of credit rating change on risk-taking

This thesis investigates whether there are changes in risk-taking behavior following an upgrade or downgrade in credit ratings. Research on effects of rating changes on capital markets is well-documented but the literature on how rating changes may affect firm behavior is sparse. Following, a downgrade in credit rating, managers may increase risk-taking to improve their overall performance or reduce risk-taking following upgrades to ensure that their performance is assessed more on the basis of what they may deem success in the form of an upgrade. Using a sample of firms trading in the U.S from 1994-2013, we find evidence of change in risk-taking behavior. We use cross-sectional regressions and matching using propensity scores and Barber and Lyon (1997) methodology to measure changes in risk-taking and we do find evidence of changes in managerial risk-taking behavior. Furthermore, we find that the direction of change (increase or decrease) in some cases is dependent on the type of measure rather than the type of rating change.

Mirroring Enzymes: The Role of H-Bonding In HQuin-BAM Catalyzed Asymmetric Aza-Henry Reactions: A DFT Study into the Reactivity, Mechanism, and Origins of Selectivity

The exact mechanistic understanding of various organocatalytic systems in asymmetric reactions such as Henry and aza-Henry transformations is important for developing and designing new synthetic organocatalysts. The focus of this dissertation will be on the use of density functional theory (DFT) for studying the asymmetric aza-Henry reaction. The first part of the thesis is a detailed mechanistic investigation of a poorly understood chiral bis(amidine) (BAM) Brønsted acid catalyzed aza-Henry reaction between nitromethane and N-Boc phenylaldimine. The catalyst, in addition to acting as a Brønsted base, serves to simultaneously activate both the electrophile and the nucleophile through dual H-bonding during C-C bond formation and is thus essential for both reaction rate and selectivity. Analysis of the H-bonding interactions revealed that there was a strong preference for the formation of a homonuclear positive charge-assisted H-bond, which in turn governed the relative orientation of substrate binding. Attracted by this well-defined mechanistic investigation, the other important aspect of my PhD research addressed a detailed theoretical analysis accounting for the observed selectivity in diastereoselective versions of this reaction. A detailed inspection of the stereodetermining C-C bond forming transition states for monoalkylated nitronate addition to a range of electronically different aldimines, revealed that the origins of stereoselectivity were controlled by a delicate balance of different factors such as steric, orbital interactions, and the extent of distortion in the catalyst and substrates. The structural analysis of different substituted transition states established an interesting dependency on matching the shape and size of the catalyst (host molecule) and substrates (guest molecules) upon binding, both being key factors governing selectivity, in essence, offering an analogy to positive cooperative binding effect of catalytic enzymes and substrates in Nature. In addition, both intra-molecular (intra-host) and inter-molecular (host-guest, guest-guest) stabilizing interactions play a key role to the high π-facial selectivity. The application of dispersion-corrected functionals (i.e., ωB97X-D and B3LYP-D3) was essential for accurately modeling these stabilizing interactions, indicating the importance of dispersion effects in enantioselectivity. As a brief prelude to more extensive future studies, the influence of a triflate counterion on both reactivity and selectivity in this reaction was also addressed.

Ranking Sets of Objects

We provide a survey of the literature on ranking sets of objects. The interpretations of those set rankings include those employed in the theory of choice under complete uncertainty, rankings of opportunity sets, set rankings that appear in matching theory, and the structure of assembly preferences. The survey is prepared for the Handbook of Utility Theory, vol. 2, edited by Salvador Barberà, Peter Hammond, and Christian Seidl, to be published by Kluwer Academic Publishers. The chapter number is provisional.

In Search of Advice for Physicians in Entry-Level Medical Markets

We consider entry-level medical markets for physicians in the United Kingdom. These markets experienced failures which led to the adoption of centralized market mechanisms in the 1960's. However, different regions introduced different centralized mechanisms. We advise physicians who do not have detailed information about the rank-order lists submitted by the other participants. We demonstrate that in each of these markets in a low information environment it is not beneficial to reverse the true ranking of any two acceptable hospital positions. We further show that (i) in the Edinburgh 1967 market, ranking unacceptable matches as acceptable is not profitable for any participant and (ii) in any other British entry-level medical market, it is possible that only strategies which rank unacceptable positions as acceptable are optimal for a physician.

Ideal timing to transfer from an acute care hospital to an interdisciplinary inpatient rehabilitation program following a stroke: an exploratory study

Affiliation: Dany Gagnon & Sylvie Nadeau: École de réadaptation, Faculté de médecine, Université de Montréal & Centre de recherche interdisciplinaire en réadaptation, Institut de réadaptation de Montréal

Cooperative of Noncooperative Behavior?

In an abstract two-agent model, we show that every deterministic joint choice function compatible with the hypothesis that agents act noncooperatively is also compatible with the hypothesis that they act cooperatively. the converse is false.

A Note on Ordinally Equivalent Pareto Surfaces

Assuming at least three individuals and some regularity conditions, we construct a set S* of Pareto surfaces which is an ordinal basis of the set S of all surfaces: every surface in S is ordinally equivalent to some surface in S* and all surfaces in S* are ordinally distinct.

Manipulation via Capacities Revisited

This paper revisits manipulation via capacities in centralized two-sided matching markets. Sönmez (1997) showed that no stable mechanism is nonmanipulable via capacities. We show that non-manipulability via capacities can be equivalently described by two types of non-manipulation via capacities: non-Type-I-manipulability meaning that no college with vacant positions can manipulate by dropping some of its empty positions; and non-Type-II-manipulability meaning that no college with no vacant positions can manipulate by dropping some of its filled positions. Our main result shows that the student-optimal stable mechanism is the unique stable mechanism which is non-Type-I-manipulable via capacities and independent of truncations. Our characterization supports the use of the student-optimal stable mechanism in these matching markets because of its limited manipulability via capacities by colleges.