Embedding logical frameworks in scala

El Framework Lógico de Edimburgo ha demostrado ser una poderosa herramienta en el estudio formal de sistemas deductivos, como por ejemplo lenguajes de programación. Sin embargo su principal implementación, el sistema Twelf, carece de expresividad, obligando al programador a escribir código repetitivo. Este proyecto presenta una manera alternativa de utilizar Twelf: a través de un EDSL (Lenguaje Embebido de Dominio Específico) en Scala que permite representar firmas del Framework Lógico, y apoyándonos en Twelf como backend para la verificación, abrimos la puerta a diversas posibilidades en términos de metaprogramación. El código fuente, así como instrucciones para instalar y configurar, está accesible en https://github.com/akathorn/elfcala. ---ABSTRACT---The Edinburgh Logical Framework has proven to be to be a powerful tool in the formal study of deductive systems, such as programming languages. However, its main implementation, the Twelf system, lacks expressiveness, requiring the programmer to write repetitive code. This project presents an alternative way of using Twelf: by providing a Scala EDSL (Embedded Domain Specific Language) that can encode Logical Framework signatures and relying on Twelf as a backend for the verification, we open the door to different possibilities in terms of metaprogramming. The source code, along with instructions to install and configure, is accessible at https://github.com/akathorn/elfcala

Non uniform embedding based on relevance analysis with reduced computational complexity: application to the detection of pathologies from biosignal recordings

Nonlinear analysis tools for studying and characterizing the dynamics of physiological signals have gained popularity, mainly because tracking sudden alterations of the inherent complexity of biological processes might be an indicator of altered physiological states. Typically, in order to perform an analysis with such tools, the physiological variables that describe the biological process under study are used to reconstruct the underlying dynamics of the biological processes. For that goal, a procedure called time-delay or uniform embedding is usually employed. Nonetheless, there is evidence of its inability for dealing with non-stationary signals, as those recorded from many physiological processes. To handle with such a drawback, this paper evaluates the utility of non-conventional time series reconstruction procedures based on non uniform embedding, applying them to automatic pattern recognition tasks. The paper compares a state of the art non uniform approach with a novel scheme which fuses embedding and feature selection at once, searching for better reconstructions of the dynamics of the system. Moreover, results are also compared with two classic uniform embedding techniques. Thus, the goal is comparing uniform and non uniform reconstruction techniques, including the one proposed in this work, for pattern recognition in biomedical signal processing tasks. Once the state space is reconstructed, the scheme followed characterizes with three classic nonlinear dynamic features (Largest Lyapunov Exponent, Correlation Dimension and Recurrence Period Density Entropy), while classification is carried out by means of a simple k-nn classifier. In order to test its generalization capabilities, the approach was tested with three different physiological databases (Speech Pathologies, Epilepsy and Heart Murmurs). In terms of the accuracy obtained to automatically detect the presence of pathologies, and for the three types of biosignals analyzed, the non uniform techniques used in this work lightly outperformed the results obtained using the uniform methods, suggesting their usefulness to characterize non-stationary biomedical signals in pattern recognition applications. On the other hand, in view of the results obtained and its low computational load, the proposed technique suggests its applicability for the applications under study.

Spatial network surrogates for disentangling complex system structure from spatial embedding of nodes

ACKNOWLEDGMENTS MW and RVD have been supported by the German Federal Ministry for Education and Research (BMBF) via the Young Investigators Group CoSy-CC2 (grant no. 01LN1306A). JFD thanks the Stordalen Foundation and BMBF (project GLUES) for financial support. JK acknowledges the IRTG 1740 funded by DFG and FAPESP. MT Gastner is acknowledged for providing his data on the airline, interstate, and Internet network. P Menck thankfully provided his data on the Scandinavian power grid. We thank S Willner on behalf of the entire zeean team for providing the data on the world trade network. All computations have been performed using the Python package pyunicorn [41] that is available at https://github.com/pik-copan/pyunicorn.

Canonical simplification of finite objects, well quasi-ordered by tree embedding /

"UILU-ENG 79 1727."

Embedding partial G-designs where G is a 4-cycle with a pendant edge

Let D denote the graph consisting of a cycle of length 4 with a pendant edge. In this paper, two very different small embeddings of partial D-designs are presented. (c) 2005 Elsevier B.V. All rights reserved.

Embedding a restricted class of partial K-4-designs

Given a partial K-4-design (X, P), if x is an element of X is a vertex which occurs in exactly one block of P, then call x a free vertex. In this paper, a technique is described for obtaining a cubic embedding of any partial K-4-design with the property that every block in the partial design contains at least two free vertices.

Embedding defeasible logic into logic programming

Defeasible reasoning is a simple but efficient approach to nonmonotonic reasoning that has recently attracted considerable interest and that has found various applications. Defeasible logic and its variants are an important family of defeasible reasoning methods. So far no relationship has been established between defeasible logic and mainstream nonmonotonic reasoning approaches. In this paper we establish close links to known semantics of logic programs. In particular, we give a translation of a defeasible theory D into a meta-program P(D). We show that under a condition of decisiveness, the defeasible consequences of D correspond exactly to the sceptical conclusions of P(D) under the stable model semantics. Without decisiveness, the result holds only in one direction (all defeasible consequences of D are included in all stable models of P(D)). If we wish a complete embedding for the general case, we need to use the Kunen semantics of P(D), instead.

Embedding e-portfolios for effective lifelong learning:a case study

Lifelong learning is a ‘keystone’ of educational policies (Faure, 1972) where the emphasis on learning shifts from teacher to learner. Higher Education (HE) institutions should be committed to developing lifelong learning, that is promoting learning that is flexible, diverse and relevant at different times, and in different places, and is pursued throughout life. Therefore the HE sector needs to develop effective strategies to encourage engagement in meaningful learning for diverse student populations. The use of e-portfolios, as a ‘purposeful aggregation of digital items’ (Sutherland & Powell, 2007), can meet the needs of the student community by encouraging reflection, the recording of experiences and achievements, and personal development planning (PDP). The use of e-portfolios also promotes inclusivity in learning as it provides students with the opportunity to articulate their aspirations and take the first steps along the pathway of lifelong learning. However, ensuring the uptake of opportunities within their learning is more complex than the students simply having access to the software. Therefore it is argued here that crucial to the effective uptake and engagement of the e-portfolio is embedding it purposefully within the curriculum. In order to investigate effective implementation of e-portfolios an explanatory case study on their use was carried out, initially focusing on 3 groups of students engaged in work-based learning and professional practice. The 3 groups had e-Portfolios embedded and assessed at different levels. Group 1 did not have the e-Portfolio embedded into their curriculum nor was the e-Portfolio assessed. Group 2 had the e-Portfolio embedded into the curriculum and formatively assessed. Group 3 also had the e-Portfolio embedded into the curriculum and were summatively assessed. Results suggest that the use of e-Portfolios needs to be integral to curriculum design in modules rather than used as an additional tool. In addition to this more user engagement was found in group 2 where the e-Portfolio was formatively assessed only. The implications of this case study are further discussed in terms of curriculum development.

Embodying and embedding children's sleep: some sociological comments and observations

This paper, drawing on our own research findings data, explores the embodiment and embedment of sleeping in children's everyday/night lives. Key themes here include children's attitudes and feelings toward the dormant body, the processes, routines and rituals associated with going to bed and going to sleep, issues associated with bedrooms and privacy, and finally the relationship between dormancy and domicile. This in turn provides the basis, in the remainder of the paper, for a further series of reflections on the mutually informing relations between the sociology of sleep and the sociology of childhood. Remaining questions and challenges involved in researching children's sleep are also considered. Sleep, it is concluded, is not simply a rich and fascinating sociological topic in its own right it also has the potential to shed valuable new light on a significant yet hitherto under-researched part of children's lives, contributing important new insights in doing so.