In this thesis we examine the relationship between hypersequent and some types of labelled sequent calculi for a subset of intermediate logics—logics between intuitionistic (Int), and classical logics—that have geometric Kripke semantics, which we call Int∗/Geo. We introduce a novel calculus for a fragment of first-order classical logic, which we call partially-shielded formulae (or PSF for short), that is adequate for expressing the semantic validity of formulae in Int∗/Geo, and apply techniques from correspondence theory to provide translations of hypersequents, simply labelled sequents and relational sequents (simply labelled sequents with relational formulae) into PSF. Using these translations, we show that hypersequents and simply labelled sequents for calculi in Int∗/Geo share the same models. We also use these translations to justify various techniques that we introduce for translating simply labelled sequents into relational sequents and vice versa. In particular, we introduce a technique called "transitive unfolding" for translating relational sequents into simply labelled sequents (and by extension, hypersequents) which preserves linear models in Int∗/Geo. We introduce syntactic translations between hypersequent calculi and simply labelled sequent calculi. We apply these translations to a novel hypersequent framework HG3ipm∗ for some logics in Int∗/Geo to obtain a corresponding simply labelled sequent framework LG3ipm∗, and to an existing simply labelled calculus for Int from the literature to obtain a novel hypersequent calculus for Int. We introduce methods for translating a simply labelled sequent calculus into a cor- responding relational calculus, and apply these methods to LG3ipm∗ to obtain a novel relational framework RG3ipm∗ that bears similarities to existing calculi from the literature. We use transitive unfolding to translate proofs in RG3ipm∗ into proofs in LG3ipm∗ and HG3ipm∗ with the communication rule, which corresponds to the semantic restriction to linear models.

A multiple-valued function is a "function" that assumes two or more distinct values in its range for at least one point in its domain. While these "functions" are not functions in the normal sense of being single-valued, the usage is so common that there is no way to dislodge it. This thesis is devoted to a particular class of multiple-valued functions: Q-valued functions. A Q-valued function is essentially a rule assigning Q unordered and not necessarily distinct points of R^n to each element of R^m. This object is one of the key ingredients of Almgren's 1700 pages proof that the singular set of an m-dimensional mass minimizing integral current in R^n has dimension at most m-2. We start by developing a decomposition theory and show for instance when a continuous Q-valued function can or cannot be seen as Q "glued" continuous classical functions. Then, the decomposition theory is used to prove intrinsically a Rademacher type theorem for Lipschitz Q-valued functions. A couple of Lipschitz extension theorems are also obtained for partially defined Lipschitz Q-valued functions. The second part is devoted to a Peano type result for a particular class of nonconvex-valued differential inclusions. To the best of the author's knowledge this is the first theorem, in the nonconvex case, where the existence of a continuously differentiable solution is proved under a mere continuity assumption on the corresponding multifunction. An application to a particular class of nonlinear differential equations is included. The third part is devoted to the calculus of variations in the multiple-valued framework. We define two different notions of Dirichlet nearly minimizing Q-valued functions, generalizing Dirichlet energy minimizers studied by Almgren. Hölder regularity is obtained for these nearly minimizers and we give some examples showing that the branching phenomena can be much worse in this context.

In this dissertation we investigate the behavior of radially symmetric non-Euclidean plates of thickness t with constant negative Gaussian curvature. We present a complete study of these plates using the Föppl-von Kármán and Kirchhoff reduced theories of elasticity. Motivated by experimental results, we focus on deformations with a periodic profile. For the Föppl-von Kármán model, we prove rigorously that minimizers of the elastic energy converge to saddle shaped isometric immersions. In studying this convergence, we prove rigorous upper and lower bounds for the energy that scale like the thickness t squared. Furthermore, for deformation with n-waves we prove that the lower bound scales like nt² while the upper bound scales like n²t². We also investigate the scaling with thickness of boundary layers where the stretching energy is concentrated with decreasing thickness. For the Kichhoff model, we investigate isometric immersions of disks with constant negative curvature into R³, and the minimizers for the bending energy, i.e. the L² norm of the principal curvatures over the class of W^2,2 isometric immersions. We show the existence of smooth immersions of arbitrarily large geodesic balls in H² into R³. In elucidating the connection between these immersions and the nonexistence/ singularity results of Hilbert and Amsler, we obtain a lower bound for the L^∞ norm of the principal curvatures for such smooth isometric immersions. We also construct piecewise smooth isometric immersions that have a periodic profile, are globally W^2,2, and numerically have lower bending energy than their smooth counterparts. The number of periods in these configurations is set by the condition that the principal curvatures of the surface remain finite and grow approximately exponentially with the radius of the disc.

We consider a syntactic restriction for higher-order grammars called safety that constrains occurrences of variables in the production rules according to their type-theoretic order. We transpose and generalize this restriction to the setting of the simply-typed lambda calculus, giving rise to what we call the safe lambda calculus. We analyze its expressivity and obtain a result in the same vein as Schwichtenberg's 1976 characterization of the simply-typed lambda calculus: the numeric functions representable in the safe lambda calculus are exactly the multivariate polynomials; thus conditional is not definable. We also give a similar characterization for representable word functions. We then examine the complexity of deciding beta-eta equality of two safe simply-typed terms and show that this problem is PSPACE-hard. The safety restriction is then extended to other applied lambda calculi featuring recursion and references such as PCF and Idealized Algol (IA for short). The next contribution concerns game semantics. We introduce a new concrete presentation of this semantics using the theory of traversals. It is shown that the revealed game denotation of a term can be computed by traversing some souped-up version of the term's abstract syntax tree using adequately defined traversal rules. Based on this presentation and via syntactic reasoning we obtain a game-semantic interpretation of safety: the strategy denotations of safe lambda-terms satisfy a property called P-incremental justification which says that the player's moves are always justified by the last pending opponent's move of greater order occurring in the player's view. Next we look at models of the safe lambda calculus. We show that these are precisely captured by Incremental Closed Categories. A game model is constructed and is shown to be fully abstract for safe IA. Further, it is effectively presentable: two terms are equivalent just if they have the same set of complete O-incrementally justified plays---where O-incremental justification is defined as the dual of P-incremental justification. Finally we study safety from the point of view of algorithmic game semantics. We observe that in the third-order fragment of IA, the addition of unsafe contexts is conservative for observational equivalence. This implies that all the upper complexity bounds known for the lower-order fragments of IA also hold for the safe fragment; we show that the lower-bounds remain the same as well. At order 4, observational equivalence is known to be undecidable for IA. We conjecture that for the order-4 safe fragment of IA, the problem is reducible to the DPDA-equivalence problem and is thus decidable.

Higher-order transformations are ubiquitous within data management. In relational databases, higher-order queries appear in numerous aspects including query rewriting and query specification. In XML databases, higher-order functions are natural due to the close connection of XML query languages with functional programming. The thesis investigates higher-order query languages that combine higher- order transformations with ordinary database query languages. We de- fine higher-order query languages based on Relational Algebra, Monad Algebra, and XQuery. The thesis also studies basic problems for these query languages including evaluation, containment, and type inference. We show that even though evaluating these higher-order query languages is non-elementary, there are subclasses that are polynomially reducible to evaluation for ordinary query languages. Our theoretical analysis is complemented by an implementation of the languages, our Higher-Order Mapping Evaluation System (HOMES). The system integrates querying and query transformation in a single higher- order query language. It allows users to write queries that integrate and combine query transformations. The system is implemented on top of traditional database management systems. The evaluation algorithm is optimized by a combination of subquery caching techniques from relational and XML databases and sharing detection schemes from functional programming.

Nonrigid image registration has received much attention in the medical imaging and computer vision research communities, because it enables a wide variety of applications. Feature tracking, segmentation, classification, temporal image differencing, tumour growth estimation, and pharmacokinetic modeling are examples of the many tasks that are enhanced by the use of aligned imagery. Over the years, the medical imaging and computer vision communties have developed and refined image registration techniques in parallel, often based on similar assumptions or underlying paradigms. This thesis focuses on variational registration, which comprises a subset of nonrigid image registration. It is divided into chapters that are based on fundamental aspects of the variational registration problem: image dissimilarity measures, changing overlap regions, regularizers, and computational solution strategies. Key contributions include the development of local versions of standard dissimilarity measures, the handling of changing overlap regions in a manner that is insensitive to the amount of non-interesting background information, the combination of two standard taxonomies of regularizers, and the generalization of solution techniques based on Fourier methods and the Demons algorithm for use with many regularizers. To illustrate and validate the various contributions, two sets of example imagery are used: 3D CT, MR, and PET images of the brain as well as 3D CT images of lung cancer patients.

In the spontaneous curvature model for two-phase lipid bilayer membranes the shape of vesicles is governed by a combination of an elastic bending energy and an interface energy that penalises the size of phase boundaries. Each lipid phase induces a preferred curvature to the membrane surface, and these curvatures as well as phase boundaries may lead to the development of kinks. In a rotationally symmetric setting we introduce a family of energies for smooth surfaces and phase fields for the lipid components and study convergence to a sharp-interface limit, which depends on the choice of the bending parameters of the phase field model. We prove that, if kinks are excluded, our energies $Gamma$-converge to the commonly used sharp-interface spontaneous curvature energy with the additional assumption of $C^1$-regularity across interfaces. For a choice of parameters such that kinks may appear, we obtain a limit that coincides with the $Gamma$-limit on all reasonable membranes and extends the classical model by assigning a bending energy also to kinks. We illustrate the theoretical result by some numerical examples.

The Autonomous Multi-Agent Physically Interacting Spacecraft (AMPHIS) test bed examines the problem of multiple spacecraft interacting at close proximity. This thesis contributes to this on-going research by addressing the development of the software architecture for the AMPHIS spacecraft simulator robots and the implementation of a Light Detection and Ranging (LIDAR) unit to be used for state estimation and navigation of the prototype robot. The software modules developed include: user input for simple user tasking; user output for data analysis and animation; external data links for sensors and actuators; and guidance, navigation and control (GNC). The software was developed in the SIMULINK/MATLAB environment as a consistent library to serve as stand alone simulator, actual hardware control on the robot prototype, and any combination of the two. In particular, the software enables hardware-in-the-loop testing to be conducted for any portion of the system with reliable simulation of all other portions of the system. The modularity of this solution facilitates fast proof-of-concept validation for the GNC algorithms. Two sample guidance and control algorithms were developed and are demonstrated here: a Direct Calculus of Variation method, and an artificial potential function guidance method. State estimation methods are discussed, including state estimation from hardware sensors, pose estimation strategies from various vision sensors, and the implementation of a LIDAR unit for state estimation. Finally, the relative motion of the AMPHIS test bed is compared to the relative motion on orbit, including how to simulate the on-orbit behavior using Hill's equations.

This thesis is comprised of three main parts: The Hermite-Hadamard inequality on discrete time scales, the fractional Hermite-Hadamard inequality, and Karush-Kuhn- Tucker conditions on higher dimensional discrete domains. In the first part of the thesis, Chapters 2 & 3, we define a convex function on a special time scale T where all the time points are not uniformly distributed on a time line. With the use of the substitution rules of integration we prove the Hermite-Hadamard inequality for convex functions defined on T. In the fourth chapter, we introduce fractional order Hermite-Hadamard inequality and characterize convexity in terms of this inequality. In the fifth chapter, we discuss convexity on n{dimensional discrete time scales T = T1 × T2 × ... × Tn where Ti ⊂ R , i = 1; 2,…,n are discrete time scales which are not necessarily periodic. We introduce the discrete analogues of the fundamental concepts of real convex optimization such as convexity of a function, subgradients, and the Karush-Kuhn-Tucker conditions. We close this thesis by two remarks for the future direction of the research in this area.

Dans ce travail nous étudions la complexité de certains fragments du mu-calcul selon deux points de vue: l’un syntaxique et l’autre topologique. Dans la première partie nous adoptons le point de vue syntaxique afin d'étudier le comportement du mu-calcul sur des classes restreintes de modèles. Parmi d'autres résultats, nous montrons en particulier que sur les modèles transitifs toute propriété définissable par une formule du mu-calcul est définissable par une formule sans alternance de points fixes. Pour ce qui concerne la perspective topologique, nous montrons d'abord que sur les modèles transitifs la logique modale correspond au fragment borélien du mu-calcul. Ensuite nous donnons une description effective des hiérarchies de Borel et de Wadge d'un sous-fragment sans alternance de cette logique sur les arbres binaires et vérifions que pour ce fragment les points de vue topologique et syntaxique coïncident. / In this work we study the complexity of some fragments of the modal mu-calculus from two points of view: the syntactical and the topological. In the first part of the dissertation we adopt the syntactical point of view in order to study the behavior of this formalism on some restricted classes of models. Among other results, we show that on transitive transition systems, every mu-formula is logically equivalent to an alternation free formula. For what concerns the topological point of view, we first prove that on transitive models, the modal logic is exactly the Borel fragment of the modal mu-calculus. Then we provide an effective description of the Borel and Wadge hierarchies of a sub-fragment of the alternation free fragment of the mu-calculus on binary trees. Finally we verify that for this fragment the syntactical point of view and topological point of view coincide.