arXiv subjects

Martin Berger

Publications and source records attributed to Martin Berger.

25 records · Page 2Linked to original sources

arXiv2017

Modelling homogeneous generative meta-programming

Homogeneous generative meta-programming (HGMP) enables the generation of program fragments at compile-time or run-time. We present the first foundational calculus which can model powerful HGMP languages such as Template Haskell. The calculus is designed such that we can gradually enhance it with the features needed to model many of the advanced features of real languages. As a demonstration of the flexibility of our approach, we also provide a simple type system for the calculus.

cs.PL↗

arXiv2017

Program Logics for Homogeneous Generative Run-Time Meta-Programming

This paper provides the first program logic for homogeneous generative run-time meta-programming---using a variant of MiniML by Davies and Pfenning as its underlying meta-programming language. We show the applicability of our approach by reasoning about example meta-programs from the literature. We also demonstrate that our logics are relatively complete in the sense of Cook, enable the inductive derivation of characteristic formulae, and exactly capture the observational properties induced by the operational semantics.

cs.LO↗

arXiv2014

Cathoristic logic: A modal logic of incompatible propositions

Cathoristic logic is a multi-modal logic where negation is replaced by a novel operator allowing the expression of incompatible sentences. We present the syntax and semantics of the logic including complete proof rules, and establish a number of results such as compactness, a semantic characterisation of elementary equivalence, the existence of a quadratic-time decision procedure, and Brandom's incompatibility semantics property. We demonstrate the usefulness of the logic as a language for knowledge representation.

cs.LO↗

arXiv2013

Si$Λ$ViO: A Trigger for $Λ$-Hyperons

As online trigger for events containing $Λ$ hyperons in p+p collisions at $\mathrm{3.1\,GeV}$ a silicon-based device has been designed and built. This system has been integrated close to the target region within the FOPI spectrometer at GSI and was also employed as a tracking device to improve the vertex reconstruction of secondary decays. The design of the detector components, read-out, the trigger capability as well as the tracking performance are presented. An enrichment factor of about 14 was achieved for events containing a $Λ$-hyperon candidate.

physics.ins-det↗

arXiv2009

Si$Λ$ViO: A Trigger for $Λ$-Particles

The production of bound kaon-nucleon-states (kaonic-cluster) in the reaction $p+p\to [ppK^{-}] + K^{+}$ should be investigated in a dedicated measurement at the FOPI detector system at the SIS-accelerator of GSI, by looking for the decay $ppK^{-} \to p + Λ\to p + p + π^{-}$. To select the final states, the detector system Si$Λ$ViO has been build up as a trigger for $Λ$-Hyperons. This detector consists of two layers of segmented silicon-strip-detectors, which are able to measure online the particle multiplicity. These two layers are arranged such, that most of the $Λ$-Hyperons will decay between them. The trigger signal is generated by comparing online the hit multiplicity on the two layers.

physics.ins-det↗

arXiv2009

Development of a GEM-TPC prototype

The use of GEM foils for the amplification stage of a TPC instead of a con- ventional MWPC allows one to bypass the necessity of gating, as the backdrift is suppressed thanks to the asymmetric field configuration. This way, a novel continuously running TPC, which represents one option for the PANDA central tracker, can be realized. A medium sized prototype with a diameter of 300 mm and a length of 600 mm will be tested inside the FOPI spectrometer at GSI using a carbon or lithium beam at intermediate energies (E = 1-3AGeV). This detector test under realistic experimental conditions should allow us to verify the spatial resolution for single tracks and the reconstruction capability for displaced vertexes. A series of physics measurement implying pion beams is scheduled with the FOPI spectrometer together with the GEM-TPC as well.

physics.ins-det↗

arXiv2008

Logical Reasoning for Higher-Order Functions with Local State

We introduce an extension of Hoare logic for call-by-value higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exported outside their scope, may store higher-order functions and may be used to construct complex mutable data structures. This primitive is captured logically using a predicate asserting reachability of a reference name from a possibly higher-order datum and quantifiers over hidden references. We explore the logic's descriptive and reasoning power with non-trivial programming examples combining higher-order procedures and dynamically generated local state. Axioms for reachability and local invariant play a central role for reasoning about the examples.

cs.LO↗