# Papers and Projects

### Journal Papers

#### An Empirical Study of Integration Activities in Distributions of Open Source Software

*Bram Adams, Ryan Kavanagh, Ahmed E. Hassan, and Daniel
M. German*. Empirical Software Engineering (EMSE), Springer
(March 2015). DOI:
10.1007/s10664-015-9371-y.
[PDF].

Reuse of software components, either closed or open source, is considered to be one of the most important best practices in software engineering, since it reduces development cost and improves software quality. However, since reused components are (by definition) generic, they need to be customized and integrated into a specific system before they can be useful. Since this integration is system- specific, the integration effort is non-negligible and increases maintenance costs, especially if more than one component needs to be integrated. This paper performs an empirical study of multi-component integration in the context of three successful open source distributions (Debian, Ubuntu and FreeBSD). Such distributions integrate thousands of open source components with an operating system kernel to deliver a coherent software product to millions of users worldwide. We empirically identified seven major integration activities performed by the maintainers of these distributions, documented how these activities are being performed by the maintainers, then evaluated and refined the identified activities with input from six maintainers of the three studied distributions. The documented activities provide a common vocabulary for component integration in open source distributions and outline a roadmap for future research on software integration.

### Technical Reports

#### On Coupled Logical Bisimulation for the Lambda-Calculus

*Ryan Kavanagh, Jean-Marie
Madiot*. October 2014. arXiv:1410:2833.

We study coupled logical bisimulation (CLB) to reason about contextual equivalence in the lambda-calculus. CLB originates in a work by Dal Lago, Sangiorgi and Alberti, as a tool to reason about a lambda-calculus with probabilistic constructs. We adapt the original definition to the pure lambda-calculus. We develop the metatheory of CLB in call-by-name and in call-by-value, and draw comparisons with applicative bisimulation (due to Abramsky) and logical bisimulation (due to Sangiorgi, Kobayashi and Sumii). We also study enhancements of the bisimulation method for CLB by developing a theory of up-to techniques for cases where the functional corresponding to bisimulation is not necessarily monotone.

### Term Papers

#### Explorations on the Wallace-Bolyai-Gerwien Theorem

*Ryan Kavanagh*. March 2015. [PDF]

In this survey paper, we present a proof of the Wallace-Bolyai-Gerwien theorem, namely, that any two plane polygons of the same area may be decomposed into the same number of pairwise congruent triangles. Several generalisations and closely related theorems will be considered, and an original example will be explored.

#### On Irreducible Rational Quintics

*Ryan Kavanagh*. April 2014. [PDF]

In this survey paper, we present a classification of irreducible quintics in and provide a procedure for solving quintics in Bring-Jerrard form that are irreducible over by radicals. These results are applied to several original examples.

*NB*: This paper is buggy, as exhibited by this
mathoverflow.net question.

#### A Primer on Provability Logic

*Ryan Kavanagh*. April 2012. [PDF]

The K4LR and GL systems of modal logic will be presented in the context of a Hilbert-style system of sentential logic. Löb’s theorem and Löb’s Derivability Criterion will be proven. Similarities between properties of and GL’s will be drawn, before proving that in GL can be interpreted as in Peano arithmetic by means of realisations. The soundness of this interpretation will be proven by Solovay’s arithmetical completeness theorem. From this, applications of GL will be considered, including a proof of Gödel’s Second Incompleteness Theorem.

#### Explorations on the Dimension of a Graph

*Ryan Kavanagh*. December 2011. [PDF]

Erdős, Harary and Tutte first defined the dimension of a graph as the minimum number such that can be embedded into the Euclidean -space with every edge of having length 1. Although some have since extended the definition such that only adjacent vertices may be separated by a distance of 1, this paper will focus on the original definition. No general method is known for determining the dimension of an arbitrary graph but lower and upper bounds will be proven for arbitrary graphs. A sharp upper bound will be given for -partite graphs by generalising the proofs presented by Erdős et al. for bipartite graphs and by Buckley et al. for tripartite graphs. New findings further include a lower bound and applications to various classes of graphs.