In recent years, several formalisms for program construction have appeared. One such formalism is the type theory developed by Per Martin-L f. Well suited as a theory for program construction, it makes possible the expression of both specifications and programs within the same formalism. Furthermore, the proof rules can be used to derive a correct program from a specification as well as to verify that a given program has a certain property. This book contains a thorough introduction to type theory, (...) with information on polymorphic sets, subsets, monomorphic sets, and a full set of helpful examples. (shrink)

Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in (...) a predicative way by an inductive generation and thus their properties can be proved inductively. We show however that some natural complete Heyting algebra cannot be inductively defined. (shrink)

This book is the result of a three-year study undertaken by a multidisciplinary working party of the Institute of Medical Ethic (UK). The group was chaired by a moral theologian, and its members included biological and ethological scientists, toxicologists, physicians, veterinary surgeons, an expert in alternatives to animal use, officers of animal welfare organizations, a Home Office Inspector, philosophers, and a lawyer. Coming from these different backgrounds, and holding a diversity of moral views, the members produced the agreed report as (...) a result of detailed and rigorous discussions. The book sets out facts about animal experiments and about animal abilities to experience pain, distress and anxiety. There is a detailed examination of the moral claims related to the benefits likely to accrue from animal research, and of strategies for weighing these benefits against the harm caused to animals, in order to decide whether particular research projects ought or ought not to proceed. This leads to consideration of the statutory and non-statutory controls which safeguard standards in such research. The final section explores a variety of philosophical arguments about the use of animals in research, and offers a philosophical justification for the Working Party's more practical conclusions. Written in clear, nontechnical language, this book is accessible to lay people as well as to scientists. It is the first such document to emerge from a meeting of people with such widely differing views on this highly controversial subject, and represents a major contribution towards informing and raising the quality of contemporary debate. The book is unique in drawing together material and ideas never before found in one volume. It will interest a broad spectrum of readers, from ethicists and animal rights advocates to scientific researchers and laboratory administrators, along with general readers concerned about this compelling issue. (shrink)

Martin-Löf Type Theory is both an important and practical formalization and a focus for a charismatic view of the foundations of mathematics. Per Martin-Löf's work has been of huge significance in the fields of logic and the foundations of mathematics, and has important applications in areas such as computing science and linguistics. This volume celebrates the twenty-fifth anniversary of the birth of the subject, and is an invaluable record both of areas of currentactivity and of the early development of the (...) subject. Also published for the first time is one of Per Martin-Löf's earliest papers. (shrink)

We present a formal theory of propositions and combinator terms, and in this theory we give an interpretation of Martin-Löf's type theory. The construction of the interpretation is inspired by the semantics for type theory, but it can also be viewed as a formalized realizability interpretation.

The concept of possessive power as it manifests in reproductions is the focus of criticism in this paper. The analysis utilizes both positive insights and illustrative mistakes from Beauvoir's account of maternity. An alternative notion of power is proposed to replace possessive power as proprietary control.

Translation of "Von der Armut am Geiste; ein Dialog des jungen Lukács," by Ágnes Heller. This translation originally appeared in The Philosophical Forum, Spring-Summer 1972.

We highlight the various domains of the flavivirus virulence factor NS1 and speculate on potential implications of the NS1 3D structure in understanding its role in flavivirus pathogenesis. Flavivirus non‐structural protein 1 (NS1) is a virulence factor with dual functions in genome replication and immune evasion. Crystal structures of NS1, combined with reconstructions from electron microscopy (EM), provide insight into the architecture of dimeric NS1 on cell membranes and the assembly of a secreted hexameric NS1‐lipid complex found in patient sera. (...) Three structural domains of NS1 likely have distinct roles in membrane association, replication complex assembly, and immune system avoidance. A conserved hydrophobic inner face is sequestered either on the membrane or in the interior of the secreted hexamer and contains regions implicated in viral replication. The exposed variable outer face is presented to cellular and secreted components of the immune system in infected patients and contains candidate regions for immune system modulation. We anticipate that knowledge of the distinct NS1 domains and assembly will lead to advances in elucidating virus‐host interactions mediated through NS1 and in dissecting the role of NS1 in viral genome replication. (shrink)

This volume draws together contributions from researchers whose work builds on the theory developed by Martin-Lof over the last twenty-five years.

Janet E. Smith; I Knit You in Your Mother's Womb, Christian bioethics: Non-Ecumenical Studies in Medical Morality, Volume 8, Issue 2, 1 January 2002, Pages 125–.

Cowdin and Tuohey argue for a rethinking of Catholic bioethical principles and the Church's moral authority. Citing the Second Vatican council for support, they argue that if the Church were to respect the proper autonomy of medicine, it would allow sterilizations. In this essay I argue against Cowdin and Tuohey's understanding that the Church has derived its moral laws independent of consultation with medicine and that it treats medicine simply as a source of technical expertise. I also argue that they (...) misunderstand the nature of autonomy as well as the Church's position regarding the type of autonomy they request for medicine. I will especially argue against their understanding of the principles of totality and double effect as “dispensations” from the moral order. I conclude that they have provided no grounds to cause the Church to reconsider its condemnation of all sterilizations. (shrink)

This essay explores ethical conflicts underlying the discourse of the policy debate about transracial adoption, focusing on the adoption of Black children by whites. Three underlying conflicts are analyzed, namely, the values of equality versus community, interracial community versus multiculturalism, individuality versus racial-ethnic community. The essay concludes with observations on multicultural families.

This response challenges Jensen's analysis in no substantial way. Rather, it explains more fully some of the moral character categories that Aristotle provides. It argues that Aristotle understood there to be two forms of continence: the continence that enables us to control natural appetites and “some form” of continence directed towards unnatural appetites, generally engendered by some pathology or abuse.

Fundamentals -- Beginning-of-life issues -- Reproductive technologies -- Contraception, sterilization, and natural family planning -- End-of-life issues -- Cooperation with evil -- Respect for the body -- The ten commandments for health care professionals and patients.

My assessment of Jean Porter's Natural and Divine Law is mixed. She provides a generally accurate account of the scholastic theory of natural law, since she steers clear of the erroneous notion that its understanding of "nature" was confined to the physical or biological and rightly notes that "nature" refers to the fullness of human nature. Her account of modern natural law theory is less reliable; for she ignores the work of several prominent contemporary natural law theorists and regrettably caricatures (...) the natural law theory employed in Church documents. I found most illuminating her claims that biblical themes influenced which issues became the focus of scholastic natural law. Her entire project, however, is flawed in serious ways: 1) surprisingly, in light of her previous work, she neglects nearly entirely the role of virtue in natural law theory; and 2) the trajectory of her work is designed to lead the Church to change its teaching on sexuality, even to the point of claiming that scholastic natural law theory has principles that justify homosexual celebrating of the erotic in the gay lifestyle. (shrink)

It is possible to defend the Church’s teaching that contraception is incompatible with God’s plan for sexuality in many different ways. This essay sketches the fundamental views of reality common to all the defenses and the main lines of the most prominent defenses, some based on natural law, on the theology of the body, and on the physical, psychological, and social consequences of the use of contraception. While all the defenses have merit, the argument based on the recognition that sexual (...) intercourse is meant to be a complete self-gift has a special power of its own. (shrink)