711 research outputs found
1869, Cornell University Press Podcast, Ep. 118 with Jayita Sarkar, author of Ploughshares and Swords
No full textThis episode, we speak with Jayita Sarkar, author of the new paperback and open access ebook Ploughshares and Swords: India’s Nuclear Program in the Global Cold War. Jay Sarkar is Senior Lecturer in Economic and Social History at the University of Glasgow and the Founding Director of the Global Decolonization Initiative.
We spoke to Jay about how the history of India’s first nuclear weapons test in 1974 has been overshadowed by their 1998 nuclear tests, why the conventional wisdom that India started off its nuclear program with nuclear energy first is in fact incorrect, and the strong connections between India’s nuclear program and their space program
Mechanical Verification of Refactorings
No full textIn this paper we describe the formal verification of refactorings for untyped and typed lambda-calculi. This verification is performed in the proof assistant Isabelle/HOL. Refactorings are program transformations applied to improve the design of source code. Well-structured source code is easier and cheaper to maintain, and this motivates the use of refactoring. These transformations have been implemented as programmer tools and, as with other metaprogramming tools, it is desirable that implementations of refactorings are correct. For a refactoring to be correct the refactored program must be identical in behaviour to the original program. Since refactorings are source-to-source transformations, concrete program information matters: for example, names (of variables, procedures, etc) and program layout should also be preserved by refactoring. This is a particular characteristic of refactorings since general program transformations operate over machine representations of programs, rather than readable source code. The paper describes the formalisation adopted, and the alternatives explored. It also reflects on some of the difficulties of performing such formalisations, the interaction between refactoring and phases such as type-checking and parsing, and the generation of correct implementations from mechanised proofs
An inventory model with reliability in an imperfect production process
No full textThe paper analyzes an economic manufacturing quantity (EMQ) model with price and advertising demand pattern in an imperfect production process under the effect of inflation. If the machine goes through a long-run process, it may shift from in-control state to out-of-control state. As a result, the system produces imperfect items. The imperfect items are reworked at a cost to make it as new. The production of imperfect quality items increases with time. To reduce the production of the imperfect items, the systems have to more reliable and the produced items depend on the reliability of the machinery system. In this direction, the author considers that the development cost, production cost, material cost are dependent on reliability parameter. Considering reliability as a decision variable, the author constructs an integrated profit function which is maximized by control theory. A numerical example along with graphical representation and sensitivity analysis are provided to illustrate the model. �� 2011 Elsevier Inc. All rights reserved
Clarifying and compiling C/C++ concurrency: from C++11 to POWER
No full textThe upcoming C and C++ revised standards add concurrency to the languages, for the first time, in the form of a subtle *relaxed memory model* (the *C++11 model*). This aims to permit compiler optimisation and to accommodate the differing relaxed-memory behaviours of mainstream multiprocessors, combining simple semantics for most code with high-performance *low-level atomics* for concurrency libraries. In this paper, we first establish two simpler but provably equivalent models for C++11, one for the full language and another for the subset without consume operations. Subsetting further to the fragment without low-level atomics, we identify a subtlety arising from atomic initialisation and prove that, under an additional condition, the model is equivalent to sequential consistency for race-free programs
Some multivariate linear regression testing problems with additional observations
No full textAbstractIn an earlier paper, the present author (Sarkar (1979), Calcutta Statist. Assoc. Bull.28, 47–56) proposed a similar test for a mean testing problem with additional observations on a set of correlated auxiliary variables. This idea has been extended here to cover some multivariate linear regression testing problems with the same type of additional observations on a set of correlated auxiliary variables
Mathematizing C++ concurrency
No full textShared-memory concurrency in C and C++ is pervasive in systems programming, but has long been poorly defined. This motivated an ongoing shared effort by the standards committees to specify concurrent behaviour in the next versions of both languages. They aim to provide strong guarantees for race-free programs, together with new (but subtle) relaxed-memory atomic primitives for high-performance concurrent code. However, the current draft standards, while the result of careful deliberation, are not yet clear and rigorous definitions, and harbour substantial problems in their details.
In this paper we establish a mathematical (yet readable) semantics for C++ concurrency. We aim to capture the intent of the current (`Final Committee') Draft as closely as possible, but discuss changes that fix many of its problems. We prove that a proposed x86 implementation of the concurrency primitives is correct with respect to the x86-TSO model, and describe our Cppmem tool for exploring the semantics of examples, using code generated from our Isabelle/HOL definitions.
Having already motivated changes to the draft standard, this work will aid discussion of any further changes, provide a correctness condition for compilers, and give a much-needed basis for analysis and verification of concurrent C and C++ programs
Ananda K. Coomaraswamy, Benoy Kumar Sarkar, and the Śukranīti
No full textThe English-raised Ananda K. Coomaraswamy, the twentieth century’s leading historian of Indian art, is well known for prizing tradition and anonymity and for upholding the position that visualization exercises were an essential part of the creative process. The first part of this article addresses the role of the English Arts and Crafts Movement and of such lesser-known figures as Sister Nivedita and Lionel de Fonseka in shaping Coomaraswamy’s views. The middle part consists of a discussion of the passages in the nineteenth-century Sanskrit treatise the Śukranīti that Coomaraswamy depended upon to support his opinions. The final part of the article is devoted to the writings of the sociologist Benoy Kumar Sarkar, author of the standard translation of the Śukranīti. As an opponent of the over-spiritualisation of Indian civilisation, he constructed a universal grammar of art. In this enterprise, he was heavily influenced by the American painter Max Weber
Foundational Certified Code in a Metalogical Framework
No full textFoundational certi ed code systems seek to prove untrusted programs to be safe relative to safety policies given in terms of actual machine architectures, thereby improving the systems' exibility and extensibility. Previous eorts have employed a structure wherein the proofs are expressed in the same logic used to express the safety policy. We propose an alternative structure wherein safety proofs are expressed in the Twelf metalogic, thereby eliminating from those proofs an extra layer of encoding needed in the previous accounts. Using this metalogical approach, we have constructed a complete, foundational account of safety for a fully expressive typed assembly language
Repensando la ciencia. La reconstrucción de la ciencia y de la sociedad de P. R. Sarkar
No full textFaced with the traditional or positivist science that stands outside history, culture and language, the author presents the thinking of Sarkar, who does not argue for an anti-science, anti-technology or falls into a science that would exist outside the social and political, but one within context, arguing for a new science of society. This paper raises important questions, such as: in what direction will then move social sciences: towards empathy and interpretation or towards disinterest and distance? Are we close to losing the universal perspectives as power and knowledge are localized and relativized? Or we are dealing with a new model of the real close, that becoming dominant will reformulate the categories of "science", "local" and "universal"?Frente a la ciencia tradicional o positivista que se coloca fuera de la historia, de la cultura y del lenguaje, el autor presenta el pensamiento de Sarkar, quien no argumenta por una posición anti-ciencia, anti-tecnología ni cae en una ciencia que existe fuera de lo social y lo político, sino contextualizada, abogando por una nueva ciencia de la sociedad. El trabajo plantea relevantes preguntas como: ¿En qué dirección se moverán luego las ciencias sociales: hacia la empatía e interpretación o hacia el desinterés y distancia? ¿Estamos nosotros cerca de perder los universales ya que el poder y el conocimiento son localizados y relativizados? ¿O es un nuevo modelo de lo real cercano de llegar a ser dominante que reformula estas categorías de "ciencia", "local" y "universal"
Foundational certified code in the Twelf metalogical framework
No full textFoundational certified code systems seek to prove untrusted programs to be safe relative to safety policies given in terms of actual machine architectures, thereby improving the systems' flexibility and extensibility. Using the Twelf metalogical framework, we have constructed a safety policy for the IA-32 architecture with a trusted runtime library. The safety policy is based on a formalized operational semantics. We have also developed a complete, foundational proof that a fully expressive typed assembly language satisfies that safety policy.<br/
- …
