250 research outputs found
Martha Nussbaums Anger and Forgiveness: Over vergelding en vergeving en over woede en liefde
No full textIn this article the author discusses the book Anger and Forgiveness written by the wellknown and influential American philosopher Martha Nussbaum. In the opinion of the author Anger and Forgiveness is a provocative and challenging book. In the book, Nussbaum makes a distinction between conditional and unconditional forgiveness, she relates conditional forgiveness to the logic of retribution and she disapproves retribution and, by extension, conditional forgiveness on moral grounds. Her disapproval of retribution and conditional forgiveness is related to her disapproval of (vindictive) anger, which in her opinion is intrinsic part of retribution and conditional forgiveness. According to Nussbaum, anger – transitional anger excluded – has to be replaced by unconditional love; only conduct that stems from unconditional love can be qualified as moral. Sometimes unconditional forgiveness can be seen as a form of unconditional love. Subsequently, Nussbaum applies her ideas on anger, retribution, forgiveness and love to the political domain, to which also criminal law belongs. Nussbaum pleads for a criminal law system empty of anger and retribution; in Nussbaum’s criminal law system there is only room for prevention, grace and human welfare – all stemming of unconditional love. Nussbaum’s Anger and Forgiveness offers an alternative view on concepts such as anger, retribution, forgiveness and love, concepts which are important within the context of criminal law and restorative justice. The author argues that, although the reader can certainly learn from Nussbaum’s ideas as explained in Anger and Forgiveness, the radicality of her ideas inevitably causes criticism; Nussbaum holds a very idealistic perspective that neglects the human condition. Instead of ruling out anger and retribution, the author advocates a criminal law system that is capable of canalizing anger and transforming vindictive anger into transitional anger. Furthermore, he pleads for a criminal law system that makes forgiveness possible without forcing victims to forgive. For that reason restorative justice practices need to be incorporated into the criminal law system. In sum, to a certain extent Nussbaum and Claessen share the same moral ideals, but they disagree on the path leading tot those ideals. Where Nussbaum opts for a top-down approach, Claessen opts for a bottom-up approach which respects the human condition
Finger trees explained anew, and slightly simplified (functional pearl)
No full textWe explicitly motivate the subtle intricacies of Hinze and Paterson\u27s Finger Tree datastructure, by step-wise refining a naive implementation. The result is a new explanation of how Finger Trees work and why they have the particular structure they have, and also a small simplification of the original implementation
Forgiveness in Criminal Law through Incorporating Restorative Mediation
No full textIn this monograph, the author argues for the integration of the concept of forgiveness into criminal law through incorporating restorative justice practices such as victim-offender mediation. Although forgiveness is not a purpose in itself nor can it be enforced, criminal law should provide room for forgiveness. Contrary to retribution, in the sense of channelled revenge, forgiveness has, after all, proven its practical usefulness in conflict resolution and in paving the way for reconciliation. The author contends that it is about time that criminal law is aimed at peace-making. This will inevitably entail significant changes to substantive and procedural criminal law. Ultimately, morality, law and politics should focus on achieving a harmonious, peaceful and, wherever possible, non-violent society. Civilisation is about more than merely substituting unbridled revenge by channelled revenge (retribution). The ideals glimmering on the horizon are repaying evil with goodness, restoration and forgiveness. This monograph discusses the views of several ethicists, philosophers, theologians, psychologists and legal scholars and seeks to provide answers to the following questions: what is forgiveness? How is it brought about? Are retribution and forgiveness each other’s opposites? Why is forgiveness important? Which view of mankind does it reflect? Does forgiveness belong to the public domain? How can it be shaped to fit into the criminal justice system? And what role does restorative justice play in this regard? Dr. Jacques Claessen (Maastricht, 1980) is an Associate Professor of Criminal Law at the Department of Criminal law and Criminology of the Faculty of Law at Maastricht University and serves as a substitute judge at the Limburg District Court in Maastricht, the Netherlands. In 2012, he was awarded with the very first Bianchi Restorative Justice Prize. Forewords by dr. John Blad, former Associate Professor of Criminal Law at the Faculty of Law of Erasmus University Rotterdam, and Nico Tydeman, Zen teacher and spiritual leader of the Amsterdam Zen Centre
Safety Property Verification of Cyclic Synchronous Circuits
No full textToday's most common formal verification tools for hardware are unable to deal with circuits containing combinational loops. However, in the areas of hardware compilation, circuit synthesis and circuit optimization, it is quite natural for a subclass of these loops, the so-called constructive loops, to arise. These are loops that physically exist in a circuit, but are never logically taken. In this paper, we present a method for safety property verification of circuits containing constructive combinational loops, based on propositional theorem proving and temporal induction. It can be used to just prove constructivess of circuits, but also to directly prove safety properties of the circuits. Unlike previously proposed methods, no fixed point iteration is needed, we do not have to compute reachable states, and no cycle-free representation of the circuit has to be computed
Shrinking and showing functions (Functional pearl)
No full textAlthough quantification over functions in QuickCheck properties has been supported from the beginning, displaying and shrinking them as counter examples has not. The reason is that in general, functions are infinite objects, which means that there is no sensible show function for them, and shrinking an infinite object within a finite number of steps seems impossible. This paper presents a general technique with which functions as counter examples can be shrunk to finite objects, which can then be displayed to the user. The approach turns out to be practically usable, which is shown by a number of examples. The two main limitations are that higher-order functions cannot be dealt with, and it is hard to deal with terms that contain functions as subterms
Parallel Parsing Processes
No full textWe derive a combinator library for non-deterministic parsers with a monadic interface, by means of successive refinements starting from a specification. The choice operator of the parser implements a breadth-first search rather than the more common depth-first search, and can be seen as a parallel composition between two parsing processes. The resulting library is simple and efficient for “almost deterministic” grammars, which are typical for programming languages and other computing science applications
Generating counterexamples for structural inductions by exploiting nonstandard models
No full textInduction proofs often fail because the stated theorem is noninductive, in which case the user must strengthen the theorem or prove auxiliary properties before performing the induction step. (Counter)model finders are useful for detecting non-theorems, but they will not find any counterexamples for noninductive theorems. We explain how to apply a well-known concept from first-order logic, nonstandard models, to the detection of noninductive invariants. Our work was done in the context of the proof assistant Isabelle/HOL and the counterexample generator Nitpick
A Coverage Analysis for Safety Property Lists
No full textWe present a coverage analysis that can be used in
property-based verification. The analysis helps identifying ”forgotten
cases”; scenarios where the property list under analysis
does not constrain a certain output at a certain point in time.
These scenarios can then be manually investigated, possibly leading
to new, previously forgotten properties being added. As there
often exist cases in which outputs are not supposed to be specified,
we also provide means for the specificier to annotate properties in
order to control what cases are supposed to be underconstrained.
Two main differences with earlier proposed similar analyses
exist: The presented analysis is design-independent, and it makes
an explicit distinction between intentionally and unintentionally
underspecified behavior
Embedded Languages for Describing and Verifying Hardware
No full textLava is a system for designing, specifying, verifying and implementing hardware. It is embedded in the functional programming language Haskell, which means that hardware descriptions are first-class objects in Haskell. We are thus able to use modern programming language features, such as higher-order functions, polymorphism, type classes and laziness, in hardware descriptions. <p />We present two rather different versions of Lava. One version realises the embedding by using <I>monads</I> to keep track of the information specified in a hardware description. The other version uses a new language construct, called observable sharing, which eliminates the need for monads so that descriptions are much cleaner. Adding <I>observable sharing</I> to Haskell is a non-conservative extension, meaning that some properties of Haskell are lost. We thus investigate to what extent we are still allowed to use a normal Haskell compiler or interpreter. <p />We also introduce an embedded language for specifying properties. The use of this language is two-fold. On the one hand, we can use it to specify and later formally verify properties of the described circuits. On the other hand, we can use it to specify and randomly test properties of normal Haskell programs. As a bonus, since hardware descriptions are embedded in Haskell, we can also use it to test our circuit descriptions. <p />Further, we present a method for formal verification of safety properties of circuits, based on temporal induction. Temporal induction proves a property by proving it for the initial state (base case), and, by assuming it holds for a certain state, proving it also holds for the following states (step case). It is well-known that induction can be improved by strengthening the inductive hypothesis. We propose several techniques that can automatically strengthen a given property
Abstract Safety Property Verification of Cyclic Synchronous Circuits
No full textToday’s most common formal verification tools for hardware are unable to deal with circuits containing combinational loops. However, in the areas of hardware compilation, circuit synthesis and circuit optimization, it is quite natural for a subclass of these loops, the so-called constructive loops, to arise. These are loops that physically exist in a circuit, but are never logically taken. In this paper, we present a method for safety property verification of circuits containing constructive combinational loops, based on propositional theorem proving and temporal induction. It can be used to just prove constructivess of circuits, but also to directly prove safety properties of the circuits. Unlike previously proposed methods, no fixed point iteration is needed, we do not have to compute reachable states, and no cycle-free representation of the circuit has to be computed.
- …
