1,721,017 research outputs found
Reasoning about a machine with local capabilities: Provably safe stack and return pointer management
No full text© The Author(s) 2018. Capability machines provide security guarantees at machine level which makes them an interesting target for secure compilation schemes that provably enforce properties such as control-flow correctness and encapsulation of local state. We provide a formalization of a representative capability machine with local capabilities and study a novel calling convention. We provide a logical relation that semantically captures the guarantees provided by the hardware (a form of capability safety) and use it to prove control-flow correctness and encapsulation of local state. The logical relation is not specific to our calling convention and can be used to reason about arbitrary programs.sponsorship: (This research was supported in part by the ModuRes Sapere Aude Advanced Grant from The Danish Council for Independent Research for the Natural Sciences (FNU). Dominique Devriese holds a Postdoctoral fellowship from the Research Foundation Flanders (FWO).)status: Publishe
Typed syntactic meta-programming
No full textWe present a novel set of meta-programming primitives for use in a dependently-typed functional language. The types of our meta-programs provide strong and precise guarantees about their termination, correctness and completeness. Our system supports typesafe construction and analysis of terms, types and typing contexts. Unlike alternative approaches, they are written in the same style as normal programs and use the language's standard functional computational model. We formalise the new meta-programming primitives, implement them as an extension of Agda, and provide evidence of usefulness by means of two compelling applications in the fields of datatype-generic programming and proof tactics. Copyright © 2013.sponsorship: This research is partially funded by the Research Foundation - Flanders (FWO), and by the Research Fund KU Leuven. Dominique Devriese holds a Ph.D. fellowship of the Research Foundation - Flanders (FWO). (Research Foundation - Flanders (FWO), Research Fund KU Leuven)status: Publishe
Lifting proof-relevant unification to higher dimensions
No full text© 2017 ACM. In a dependently typed language such as Coq or Agda, unification can be used to discharge equality constraints and detect impossible cases automatically. By nature of dependent types, it is necessary to use a proof-relevant unification algorithm where unification rules are functions manipulating equality proofs. This ensures their correctness but simultaneously sets a high bar for new unification rules. In particular, so far no-one has given a satisfactory proof-relevant version of the injectivity rule for indexed datatypes. In this paper, we describe a general technique for solving equations between constructors of indexed datatypes. We handle the main technical problem-generalization over equality proofs in the indices-by introducing new equations between equality proofs. Borrowing terminology from homotopy type theory, we call them higher-dimensional equations. To apply existing one-dimensional unifiers to these higher-dimensional equations, we show how unifiers can be lifted to a higher dimension. We show the usefulness of this idea by applying it to the unification algorithm used by Agda, though it can also be applied in languages that support identity types but not general indexed datatypes.sponsorship: This research is partially funded by the Research Fund KU Leuven. Jesper Cockx and Dominique Devriese respectively hold a Ph.D. fellowship and a postdoctoral fellowship of the Research Foundation - Flanders (FWO). (Research Fund KU Leuven, Research Foundation - Flanders (FWO))status: Publishe
Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory
No full textDependently typed languages such as Agda, Coq, and Idris use a syntactic first-order unification algorithm to check definitions by dependent pattern matching. However, standard unification algorithms implicitly rely on principles such as uniqueness of identity proofs and injectivity of type constructors. These principles are inadmissible in many type theories, particularly in the new and promising branch known as homotopy type theory. As a result, programs and proofs in these new theories cannot make use of dependent pattern matching or other techniques relying on unification, and are as a result much harder to write, modify, and understand. This paper proposes a proof-relevant framework for reasoning formally about unification in a dependently typed setting. In this framework, unification rules compute not just a unifier but also a corresponding soundness proof in the form of an equivalence between two sets of equations. By rephrasing the standard unification rules in a proof-relevant manner, they are guaranteed to preserve soundness of the theory. In addition, it enables us to safely add new rules that can exploit the dependencies between the types of equations, such as rules for eta-equality of record types and higher dimensional unification rules for solving equations between equality proofs. Using our framework, we implemented a complete overhaul of the unification algorithm used by Agda. As a result, we were able to replace previous ad-hoc restrictions with formally verified unification rules, fixing a substantial number of bugs in the process. In the future, we may also want to integrate new principles with pattern matching, for example, the higher inductive types introduced by homotopy type theory. Our framework also provides a solid basis for such extensions to be built on.sponsorship: Acknowledgements
We want to thank the anonymous reviewers for their hard work and insightful
comments. Dominique Devriese holds a Postdoctoral fellowship from the Research
Foundation Flanders (FWO). (Research Foundation (Flanders))status: Published onlin
Fixing idioms: A recursion primitive for applicative DSLs
No full textIn a lazy functional language, the standard encoding of recursion in DSLs uses the host language's recursion, so that DSL algorithms automatically use the host language's least fixpoints, even though many domains require algorithms to produce different fixpoints. In particular, this is the case for DSLs implemented as Applicative functors (structures with a notion of pure computations and function application).We propose a recursion primitive afix that models a recursive binder in a finally tagless HOAS encoding, but with a novel rank-2 type that allows us to specify and exploit the effectsvalues separation that characterises Applicative DSLs. Unlike related approaches for Monads and Arrows, we model effectful recursion, not value recursion. Using generic programming techniques, we define an aritygeneric version of the operator to model mutually recursive definitions. We recover intuitive user syntax with a form of shallow syntactic sugar: an alet construct that syntactically resembles the let construct, which we have implemented in the GHC Haskell compiler. We describe a proposed axiom for the afix operator. We demonstrate usefulness with examples from Applicative parser combinators and functional reactive programming. We show how higher-order recursive operators like many can be encoded without special library support, unlike previous approaches, and we demonstrate an implementation of the left recursion removal transform. Copyright © 2013 ACM.sponsorship: (This research is partially funded by the Research Foundation - Flanders (FWO), and by the Research Fund KU Leuven. Dominique Devriese holds a Ph.D. fellowship of the Research Foundation - Flanders (FWO).)status: Publishe
Partial Type Signatures for Haskell
No full textStrong type systems can be used to increase the reliability and performance of programs. In combination with type inference the overhead for the programmer can be kept small. Nevertheless, explicit type signatures often remain needed or useful. In languages with standard Hindley-Milner-based type systems, programmers have a binary choice between omitting the type signature (and rely on type inference) or explicitly providing the type entirely; there are no intermediate options. Proposals for partial type signatures exist, but none support features like local constraints and GHC's non-generalisation of local bindings. Therefore we propose and motivate a practical form of partial type signatures for present-day Haskell. We formally describe our proposal as an extension of the OutsideIn(X) system and prove some of its properties. We have developed a (not yet complete) implementation for the GHC Haskell compiler. Our design fits naturally in both the OutsideIn(X) formalism and the compiler. © 2014 Springer International Publishing.sponsorship: (Acknowledgments This research is partially funded by the Research Foundation - Flanders (FWO), and by the Research Fund KU Leuven. Dominique Devriese holds a Ph.D. fellowship of the Research Foundation - Flanders (FWO).)status: Publishe
Unifiers As Equivalences: Proof-relevant Unification of Dependently Typed Data
No full text© 2016 ACM. Dependently typed languages such as Agda, Coq and Idris use a syntactic first-order unification algorithm to check definitions by dependent pattern matching. However, these algorithms don't adequately consider the types of the terms being unified, leading to various unintended results. As a consequence, they require ad hoc restrictions to preserve soundness, but this makes them very hard to prove correct, modify, or extend. This paper proposes a framework for reasoning formally about unification in a dependently typed setting. In this framework, unification rules compute not just a unifier but also a corresponding correctness proof in the form of an equivalence between two sets of equations. By rephrasing the standard unification rules in a proofrelevant manner, they are guaranteed to preserve soundness of the theory. In addition, it enables us to safely add new rules that can exploit the dependencies between the types of equations. Using our framework, we reimplemented the unification algorithm used by Agda. As a result, we were able to replace previous ad hoc restrictions with formally verified unification rules, fixing a number of bugs in the process. We are convinced this will also enable the addition of new and interesting unification rules in the future, without compromising soundness along the way.sponsorship: Jesper Cockx and Dominique Devriese respectively hold a Ph.D. fellowship and a postdoctoral fellowship of the Research Foundation - Flanders (FWO). (Research Foundation - Flanders (FWO))status: Publishe
Experience Report: Functional Reactive Programming and the DOM
No full text© 2017 ACM. Web applications are inherently event-driven and traditionally implemented using imperative callbacks in Javascript. An alternative approach for such programs is functional reactive programming (FRP). FRP offers abstractions to make event-driven programming convenient, safe and composable, but like pure functions it is isolated from the 'outside' world. In this paper we describe our experience in developing a library that binds FRP to the document object model (DOM). We describe that in its current state there are fundamental issues that do not yet have a perfect solution. We expand upon the functionality of existing FRP DOM libraries with an FRP model for DOM properties. We show that despite of some design problems a pragmatic library can be created that can be used to create web applications.sponsorship: (Bob Reynders holds an SB fellowship of the Research Foundation - Flanders (FWO). Dominique Devriese holds a postdoctoral fellowship of the Research Foundation - Flanders (FWO). This research was partially funded by the SBO project TEARLESS.)status: Publishe
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
