<p>Consider the standard graded polynomial ring in $n$ variables over a field $k$ and fix the Hilbert function of a homogeneous ideal. In the nineties Bigatti, Hulett, and Pardue showed that the Hilbert scheme consisting of all the homogeneous ideals with such a Hilbert function contains an extremal point which simultaneously maximizes all the graded Betti numbers. Such a point is the unique lexsegment ideal associated to the fixed Hilbert function.</p> <p> For such a scheme, we consider the individual strata defined by all ideals with Castelnuovo-Mumford regularity bounded above by <em>m</em>. In 1997 Mall showed that when <em>k </em>is of characteristic 0 there exists an ideal in each nonempty strata with maximal possible Betti numbers among the ideals of the strata. In chapter 4 of this thesis we provide a new construction of Mall's ideal, extend the result to fields of any characteristic, and show that these ideals have other extremal properties. For example, Mall's ideals satisfy an equation similar to Green's hyperplane section theorem.</p> <p> The key technical component needed to extend the results of Mall is discussed in Chapter 3. This component is the construction of a new invariant called the distraction-generic initial ideal. Given a homogeneous ideal <em>I C S</em> we construct the associated distraction-generic initial ideal, D-gin_< (<em>I</em>), by iteratively computing initial ideals and general distractions. The result is a monomial ideal that is strongly stable in any characteristic and which has many properties analogous to the generic initial ideal of <em>I</em>.</p>

<p dir="ltr">We develop a cyclic theory for categorical coalgebras and show that, when applied to the categorical coalgebra of singular chains on a space, this provides an algebraic model for its free loop space as an S¹-space. In other words, the natural circle action on loop spaces, given by rotation of loops, is encoded in the algebraic structure. In particular, the cyclic homology of the categorical coalgebra of singular chains on a topological space X is isomorphic to the S¹-equivariant homology of the free loop space. This extends known results relating cyclic theories for the algebra of chains on the based loop space and the equivariant homology of its free loop space. In fact, our statements do not require X to be simply connected, and we work over an arbitrary commutative ring. Along the way, we introduce a family of polytopes, coined as Goodwillie polytopes, that control the combinatorics behind the relationship of the coHochschild complex of a categorical coalgebra and the Hochschild complex of its associated differential graded category.</p>

<div>The rapid development of topology optimization in photonics has greatly expanded the number of photonic structures with extraordinary performance. The optimization is usually solved by using a gradient-based optimization algorithm, where gradients are evaluated by the adjoint sensitivity analysis. While the adjoint sensitivity analysis has been demonstrated to provide reliable gradients for designs of dielectrics, there has not been too much success in plasmonics. The difficulty of obtaining accurate field solutions near sharp edges and corners in plasmonic structures, and the strong field enhancement jointly increase the numerical error of gradients, leading to failure of convergence for any gradient-based algorithm. </div><div> </div><div>We present a new method of calculating accurate sensitivity with the FDTD method by direct differentiation of the time-marching system in frequency domain. This new method supports general frequency-domain objective functions, does not relay on implementation details of the FDTD method, works with general isotropic materials and can be easily incorporated into both level-set-based and density-based topology optimizations. The method is demonstrated to have superior accuracy compared to the traditional continuous sensitivity. Next, we present a framework to carry out density-based topology optimization using our new sensitivity formula. We use the non-linear material interpolation to counter the rough landscape of plasmonics, adopt the filteringand-projection regularization to ensure manufacturability and perform the optimization with a continuation scheme to improve convergence. </div><div> </div><div>We give two examples involving reconstruction of near fields of plasmonic structures to illustrate the robustness of the sensitivity formula and the optimization framework. In the end, we apply our method to generate a rectangular temperature profile in the recording medium of the HAMR system. </div>

Many e-voting techniques have been proposed but not widely used in reality. One of the problems associated with most of existing e-voting techniques is the lack of transparency, leading to a failure to deliver voter assurance. In this work, we propose a transparent, auditable, end-to-end verifiable, and mutual restraining e-voting protocol that exploits the existing multi-party political dynamics such as in the US. The new e-voting protocol consists of three original technical contributions -- universal verifiable voting vector, forward and backward mutual lock voting, and in-process check and enforcement -- that, along with a public real time bulletin board, resolves the apparent conflicts in voting such as anonymity vs. accountability and privacy vs. verifiability. Especially, the trust is split equally among tallying authorities who have conflicting interests and will technically restrain each other. The voting and tallying processes are transparent to voters and any third party, which allow any voter to verify that his vote is indeed counted and also allow any third party to audit the tally. For the environment requiring receipt-freeness and coercion-resistance, we introduce additional approaches to counter vote-selling and voter-coercion issues. Our interactive voting protocol is suitable for small number of voters like boardroom voting where interaction between voters is encouraged and self-tallying is necessary; while our non-interactive protocol is for the scenario of large number of voters where interaction is prohibitively expensive. Equipped with a hierarchical voting structure, our protocols can enable open and fair elections at any scale.

<div>Given a parametrized family of Iterated Function System (IFS) we give sufficient conditions for a parameter on the boundary of the connectedness locus, M, to be accessible from the complement of M.</div><div>Moreover, we provide a few examples of such parameters and describe how they are connected to Misiurewicz parameter in the Mandelbrot set, i.e. the connectedness locus of the quadratic family z^2+c.<br></div>

The use of formal methods in software development seeks to increase our confidence in the resultant system. Their use often requires tool support, so the integrity of a development using formal methods is dependent on the integrity of the tool-set used. Specifically its integrity depends on the theorem prover, since in a typical formal development system the theorem prover is used to establish the validity of the proof obligations incurred by all the steps in the design and refinement process. In this thesis we are concerned with tool-based formal development systems that are used to develop high-integrity software. Since the theorem prover program is a critical part of such a system, it should ideally have been itself formally verified. Unfortunately, most theorem provers are too complex to be verified formally using currently available techniques. An alternative approach, which has many advantages, is to include a proof checker as an extra component in the system, and to certify this. A proof checker is a program which reads and checks the proofs produced by a theorem prover. Proof checkers are inherently simpler than theorem provers, since they only process actual proofs, whereas much of the code of a theorem prover is concerned with searching the space of possible proofs to find the required one. They are also free from all but the simplest user interface concerns, since their input is a proof produced by another program, and their output may be as simple as a `yes/no' reply to the question: Is this a valid proof? plus a list of assumptions on which this judgement is based. When included in a formal development system a stand-alone proof checker is, in one sense, superfluous, since it does not produce any proofs -- the theorem prover does this. Instead its importance is in establishing the integrity of the results of the system -- it provides extra assurance. A proof checker provides extra assurance simply by checking the proofs, since all proofs have then been validated by two independent programs. However a proof checker can provide an extra, and higher, level of assurance if it has been formally verified. In order for formal verification to be feasible the proof checker must be as simple as possible. In turn the simplicity of a proof checker is dependent on the complexity of the data which it processes, that is, the representation of the proofs that it checks. This thesis develops a representation of proofs that is simple and generic. The aim is to produce a generic representation that is applicable to the proofs produced by a variety of theorem provers. Simplicity facilitates verification, while genericity maximises the return on the effort of verification. Using a generic representation places obligations on the theorem provers to produce a proof record in this format. A flexible recorder/translator architecture is proposed which allows proofs to be recorded by existing theorem provers with minimal changes to the original code. The prover is extended with a recorder module whose output is then, if necessary, converted to the generic format by a separate translator program. A formal specification of a checker for proofs recorded in this representation is given. The specification could be used to formally develop a proof-checker, although this step is not taken in this thesis. In addition the characteristics of both the specification and possible implementations are investigated. This is done to assess the size and feasibility of the verification task, and also to confirm that the design is not over-sensitive to the size of proofs. This investigation shows that a checker developed from the specification will be scalable to handle large proofs. To investigate the feasibility of a system based on this architecture, prototype proof recorders were developed for the Ergo 5 and Isabelle 98 theorem provers. In addition a prototype checker was written to check proofs in the proposed format. This prototype is compatible with the formal specification. The combined system was tested successfully using existing proofs for both the Ergo 5 and Isabelle 98 theorem provers.

This thesis details the development of a model of driver behaviour at railway level crossings that allows the probability of an accident under different conditions and interventions to be calculated. A method for classifying different crossings according to their individual risk levels is also described.

<p>This work explores how randomization can be exploited to deliver sophisticated</p><p>algorithms with provable bounds for: (i) The approximation of matrix functions, such</p><p>as the log-determinant and the Von-Neumann entropy; and (ii) The low-rank approximation</p><p>of matrices. Our algorithms are inspired by recent advances in Randomized</p><p>Numerical Linear Algebra (RandNLA), an interdisciplinary research area that exploits</p><p>randomization as a computational resource to develop improved algorithms for</p><p>large-scale linear algebra problems. The main goal of this work is to encourage the</p><p>practical use of RandNLA approaches to solve Big Data bottlenecks at industrial</p><p>level. Our extensive evaluation tests are complemented by a thorough theoretical</p><p>analysis that proves the accuracy of the proposed algorithms and highlights their</p><p>scalability as the volume of data increases. Finally, the low computational time and</p><p>memory consumption, combined with simple implementation schemes that can easily</p><p>be extended in parallel and distributed environments, render our algorithms suitable</p><p>for use in the development of highly efficient real-world software.</p>

<div>This dissertation is based on joint work with Monte Cooper and is broken into two main parts, both of which study the defining ideals of the Rees rings of determinantal and Pfaffian ideals of generic height. In both parts, we attempt to place degree bounds on the defining equations.</div><div> </div><div> The first part of the dissertation consists of Chapters 3 to 5. Let $R = K[x_{1},\ldots,x_{d}]$ be a standard graded polynomial ring over a field $K$, and let $I$ be a homogeneous $R$-ideal generated by $s$ elements. Then there exists a polynomial ring $\mathcal{S} = R[T_{1},\ldots,T_{s}]$, which is also equal to $K[x_{1},\ldots,x_{d},T_{1},\ldots,T_{s}]$, of which the defining ideal of $\mathcal{R}(I)$ is an ideal. The polynomial ring $\mathcal{S}$ comes equipped with a natural bigrading given by $\deg x_{i} = (1,0)$ and $\deg T_{j} = (0,1)$. Here, we attempt to use specialization techniques to place bounds on the $x$-degrees (first component of the bidegrees) of the defining equations, i.e., the minimal generators of the defining ideal of $\mathcal{R}(I)$. We obtain degree bounds by using known results in the generic case and specializing. The key tool are the methods developed by Kustin, Polini, and Ulrich to obtain degree bounds from approximate resolutions. We recover known degree bounds for ideals of maximal minors and submaximal Pfaffians of an alternating matrix. Additionally, we obtain $x$-degree bounds for sufficiently large $T$-degrees in other cases of determinantal ideals of a matrix and Pfaffian ideals of an alternating matrix. We are unable to obtain degree bounds for determinantal ideals of symmetric matrices due to a lack of results in the generic case; however, we develop the tools necessary to obtain degree bounds once similar results are proven for generic symmetric matrices.</div><div> </div><div> The second part of this dissertation is Chapter 6, where we attempt to find a bound on the $T$-degrees of the defining equations of $\mathcal{R}(I)$ when $I$ is a nonlinearly presented homogeneous perfect Gorenstein ideal of grade three having second analytic deviation one that is of linear type on the punctured spectrum. We restrict to the case where $\mathcal{R}(I)$ is not Cohen-Macaulay. This is a natural next step following the work of Morey, Johnson, and Kustin-Polini-Ulrich. Based on extensive computation in Macaulay2, we give a conjecture for the relation type of $I$ and provide some evidence for the conjecture. In an attempt to prove the conjecture, we obtain results about the defining ideals of general fibers of rational maps, which may be of independent interest. We end with some examples where the bidegrees of the defining equations exhibit unusual behavior.</div>

<div>On rectangular meshes, the simplest spectral element method for elliptic equations is the classical Lagrangian <i>Q</i>^k finite element method with only (<i>k</i>+1)-point Gauss-Lobatto quadrature, which can also be regarded as a finite difference scheme on all Gauss-Lobatto points. We prove that this finite difference scheme is (<i>k</i> + 2)-th order accurate for <i>k</i> ≥ 2, whereas <i>Q</i>^<i>k</i> spectral element method is usually considered as a (<i>k</i> + 1)-th order accurate scheme in <i>L²</i>-norm. This result can be extended to linear wave, parabolic and linear Schrödinger equations.</div><div><br></div><div><div>Additionally, the <i>Q^k</i> finite element method for elliptic problems can also be viewed as a finite difference scheme on all Gauss-Lobatto points if the variable coefficients are replaced by their piecewise <i>Q^k </i>Lagrange interpolants at the Gauss Lobatto points in each rectangular cell, which is also proven to be (<i>k</i> + 2)-th order accurate.</div></div><div><br></div><div><div>Moreover, the monotonicity and discrete maximum principle can be proven for the fourth order accurate Q2 scheme for solving a variable coefficient Poisson equation, which is the first monotone and high order accurate scheme for a variable coefficient elliptic operator.</div></div><div><br></div><div><div>Last but not the least, we proved that certain high order accurate compact finite difference methods for convection diffusion problems satisfy weak monotonicity. Then a simple limiter can be designed to enforce the bound-preserving property when solving convection diffusion equations without losing conservation and high order accuracy.</div><div><br></div></div>