Presentations for monoids of finite partial isometries

In this paper we give presentations for the monoid DPn of all partial isometries on {1,..., n} and for its submonoid ODPn of all order-preserving partial isometries.

Normally ordered semigroups

Glasgow Mathematical Journal, nº 50 (2008), p. 325-333

A framework to operate transformations between distinct models differing in modelling concepts

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para obtenção do grau de Mestre em Engenharia Electrotécnica e de Computadores

Deciding Kleene Algebra Terms Equivalence in Coq

This paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial derivatives and does not require the construction of the corresponding automata. Recent theoretical and experimental research provides evidence that this method is, on average, more efficient than the classical methods based on automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalization of the algorithm to decide the equivalence of terms of Kleene algebra with tests. The motivation for the work presented in this paper is that of using the libraries developed as trusted frameworks for carrying out certified program verification.

A framework for efficient model transformations

The reported productivity gains while using models and model transformations to develop entire systems, after almost a decade of experience applying model-driven approaches for system development, are already undeniable benefits of this approach. However, the slowness of higher-level, rule based model transformation languages hinders the applicability of this approach to industrial scales. Lower-level, and efficient, languages can be used but productivity and easy maintenance seize to exist. The abstraction penalty problem is not new, it also exists for high-level, object oriented languages but everyone is using them now. Why is not everyone using rule based model transformation languages then? In this thesis, we propose a framework, comprised of a language and its respective environment, designed to tackle the most performance critical operation of high-level model transformation languages: the pattern matching. This framework shows that it is possible to mitigate the performance penalty while still using high-level model transformation languages.

A logical foundation for session-based concurrent computation

Linear logic has long been heralded for its potential of providing a logical basis for concurrency. While over the years many research attempts were made in this regard, a Curry-Howard correspondence between linear logic and concurrent computation was only found recently, bridging the proof theory of linear logic and session-typed process calculus. Building upon this work, we have developed a theory of intuitionistic linear logic as a logical foundation for session-based concurrent computation, exploring several concurrency related phenomena such as value-dependent session types and polymorphic sessions within our logical framework in an arguably clean and elegant way, establishing with relative ease strong typing guarantees due to the logical basis, which ensure the fundamental properties of type preservation and global progress, entailing the absence of deadlocks in communication. We develop a general purpose concurrent programming language based on the logical interpretation, combining functional programming with a concurrent, session-based process layer through the form of a contextual monad, preserving our strong typing guarantees of type preservation and deadlock-freedom in the presence of general recursion and higher-order process communication. We introduce a notion of linear logical relations for session typed concurrent processes, developing an arguably uniform technique for reasoning about sophisticated properties of session-based concurrent computation such as termination or equivalence based on our logical approach, further supporting our goal of establishing intuitionistic linear logic as a logical foundation for sessionbased concurrency.

Photochemical synthesis and functional transformations of bicyclic vinyl aziridines

Aziridines, a class of organic compounds containing a three membered heterocycle with a nitrogen atom, are extremely valuable molecules in organic and medicinal chemistry. They are frequently used as versatile precursors in the synthesis of natural products, and many biologically active molecules possess the aziridine moiety. The reactivity of aziridines has been studied, for example, in ring-opening reactions with thiols. However, not much interest seems to be given to reactions of aziridines in aqueous media, despite the numberless advantages of using water as solvent in organic chemistry. The nucleophilic ring-opening reaction of aziridines in aqueous media was here explored. Following the Kaplan aziridine synthetic methodology, in which pyridinium salts undergo a photochemical transformation to give bicyclic vinyl aziridines, new aziridines were synthetized. Their nucleophilic ring-opening reaction in water under physiological conditions was investigated and a range of sulphur, nitrogen, carbon and oxygen nucleophiles tested. Thiols, anilines and azide proved to be good nucleophiles to react with the aziridines, giving the ring-opening product in moderate to good yields. The best results were obtained with thiols, more specifically with cysteine-derived nucleophiles. Preliminary results show that these bicyclic vinyl aziridines can modify calcitonin, a peptide containing two cysteine amino acids residues, grating them the potential to be used in bioconjugation as ligands to cysteine-containing proteins, or even as enzyme inhibitors of, for example, cysteine proteases. Additionally, exploratory investigations suggest that the separation of both enantiomers of the bicyclic vinyl aziridine can be performed by taking advantage of an enzymatic methodology for the resolution of racemic secondary alcohols. Both enantiomers would be highly valuable as precursors in the synthesis of enantiomerically pure molecules, as no other method is currently reported for their separation.

On mappings preserving the sharp and star orders

The present paper is devoted to the study of linear maps preserving certain relations, such as the sharp partial order and the star partial order in semisimple Banach algebras and C*-algebras.

ADSNARK: Nearly practical and privacy-preserving proofs on authenticated data

We study the problem of privacy-preserving proofs on authenticated data, where a party receives data from a trusted source and is requested to prove computations over the data to third parties in a correct and private way, i.e., the third party learns no information on the data but is still assured that the claimed proof is valid. Our work particularly focuses on the challenging requirement that the third party should be able to verify the validity with respect to the specific data authenticated by the source — even without having access to that source. This problem is motivated by various scenarios emerging from several application areas such as wearable computing, smart metering, or general business-to-business interactions. Furthermore, these applications also demand any meaningful solution to satisfy additional properties related to usability and scalability. In this paper, we formalize the above three-party model, discuss concrete application scenarios, and then we design, build, and evaluate ADSNARK, a nearly practical system for proving arbitrary computations over authenticated data in a privacy-preserving manner. ADSNARK improves significantly over state-of-the-art solutions for this model. For instance, compared to corresponding solutions based on Pinocchio (Oakland’13), ADSNARK achieves up to 25× improvement in proof-computation time and a 20× reduction in prover storage space.

Green's relations, regularity and abundancy for semigroups of quasi-onto transformations

Let V be an infinite-dimensional vector space and for every infinite cardinal n such that n≤dimV, let AE(V,n) denote the semigroup of all linear transformations of V whose defect is less than n. In 2009, Mendes-Gonçalves and Sullivan studied the ideal structure of AE(V,n). Here, we consider a similarly-defined semigroup AE(X,q) of transformations defined on an infinite set X. Quite surprisingly, the results obtained for sets differ substantially from the results obtained in the linear setting.

Las transformaciones de la burocracia provincial: capacidades del Estado en la provincia de Córdoba. Transformations of provincial bureaucracy: State´s capacities in the province of Córdoba.

A partir de las políticas de descentralización llevadas adelante en Argentina desde la década de los ochenta, las provincias han adquirido desde entonces una importante serie de nuevas funciones lo cual las ha obligado a ampliar y diversificar sus estructuras burocráticas y administrativas. Lo que este proyecto busca abordar es un análisis de las transformaciones ocurridas durante los últimos veinte años en la organización burocrática del estado provincial en Córdoba. El proyecto pretende indagar dos aspectos de la organización burocrática: por un lado, el diseño organizacional institucional (leyes de Ministerios) y la división del trabajo que ello implica; y por otro lado, los principales procesos administrativos transversales que articulan funcionalmente las diferentes áreas de la burocracia provincial (administración financiera y recursos humanos). A partir de ello nos interesa poner en relación estas transformaciones con los cambios que va experimentando la agenda gubernamental. Suponemos, en este sentido, que los cambios organizacionales responden a cambios en dicha agenda y a la relación de fuerzas políticas que va implícita en la conformación de las mismas. De este modo, nuestra hipótesis plantea que los cambios organizaciones generados por la transformación de las agendas se manifiestan de forma más inmediata en la dimensión del diseño organizacional, mientras que los procesos administrativos transversales experimentan cambios más graduales y no necesariamente vinculados a las transformaciones de la primera dimensión. El objetivo general es analizar las transformaciones de la Administración Pública Provincial (APP) en la provincia de Córdoba, a través de dos dimensiones (el diseño de la organización burocrática y los procesos administrativos transversales), desde el retorno a la democracia (1983) a la actualidad. La investigación será realizada a la luz de posturas epistemológicas y metodológicas que en las ciencias sociales sustentan la triangulación de métodos. Recurriremos tanto a fuentes documentales y estadísticas para reconstruir el proceso de transformación de la APP, como a entrevistas semiestructuradas con actores claves para indagar sobre las dimensiones identificadas en el proyecto. Se encuadra en lo que metodológicamente se denomina "estudio de caso". La investigación permitirá fortalecer el estudio de la administración y las organizaciones públicas, lo que representa una tarea altamente significativa (y necesaria) para el mejoramiento del sector público y las necesidades de la ciudadanía. El impacto esperable es la explicitación y sistematización de las transformaciones del aparato burocrático, que puedan ser observadas, mejoradas y desarrolladas por el conjunto de las carteras ministeriales, y la confección de estrategias y tecnologías de gestión que permitan incrementar las capacidades de la administración pública provincial en la realización de las políticas y la resolución de los problemas sociales.

The naturalist's guide in collecting and preserving objects of natural history, with a complete catalogue of the birds of the eastern Massachusetts.

[1873 printing]

Approved Drug Products with Theurapeutic Equivalence Evaluation - 34th edition

The publication, Approved Drug Products with Therapeutic Equivalence Evaluations (the List, commonly known as the Orange Book), identifies drug products approved on the basis of safety and effectiveness by the Food and Drug Administration (FDA) under the Federal Food, Drug, and Cosmetic Act (the Act). Drugs on the market approved only on the basis of safety (covered by the ongoing Drug Efficacy Study Implementation [DESI] review [e.g., Donnatal® Tablets and Librax® Capsules] or pre-1938 drugs [e.g., Phenobarbital Tablets]) are not included in this publication. The main criterion for the inclusion of any product is that the product is the subject of an application with an effective approval that has not been withdrawn for safety or efficacy reasons. Inclusion of products on the List is independent of any current regulatory action through administrative or judicial means against a drug product. In addition, the List contains therapeutic equivalence evaluations for approved multisource prescription drug products. These evaluations have been prepared to serve as public information and advice to state health agencies, prescribers, and pharmacists to promote public education in the area of drug product selection and to foster containment of health care costs. Therapeutic equivalence evaluations in this publication are not official FDA actions affecting the legal status of products under the Act.