| 1. |
- Benaissa, Zine El-Abidine, et al.
(författare)
-
Logical Modalities and Multi-Stage Programming
- 1999
-
Konferensbidrag (refereegranskat)abstract
- Multi-stage programming is a method for improving the performance of programs through the introduction of controlled program specialization. This paper makes a case for multi-stage programming with open code and closed values. We argue that a simple language exploiting interactions between two logical modalities is well suited for multi-stage programming, and report the results from our study of categorical models for multi-stage languages.
|
|
| 2. |
- Calcagno, Cristiano, et al.
(författare)
-
Closed Types as a Simple Approach to Safe Imperative Multi-Stage Programming
- 2000
-
Ingår i: Automata, Languages and Programming. - Heidelberg : Springer. - 9783540677154 - 9783540450221 ; , s. 25-36
-
Konferensbidrag (refereegranskat)abstract
- Safely adding computational effects to a multi-stage language has been an open problem. In previous work, a closed type constructor was used to provide a safe mechanism for executing dynamically generated code. This paper proposes a general notion of closed type as a simple approach to safely introducing computational effects into multi-stage languages. We demonstrate this approach formally in a core language called Mini-MLref BN. This core language combines safely multi-stage constructs and ML-style references. In addition to incorporating state, Mini-ML ref BN also embodies a number of technical improvements over previously proposed core languages for multi-stage programming.
|
|
| 3. |
- Calcagno, Cristiano, et al.
(författare)
-
ML-like Inference for Classifiers
- 2004
-
Ingår i: Programming Languages and Systems. - Heidelberg : Springer Berlin/Heidelberg. - 9783540213130 - 9783540247258 ; , s. 79-93
-
Konferensbidrag (refereegranskat)abstract
- Environment classifiers were proposed as a new approach to typing multi-stage languages. Safety was established in the simply-typed and let-polymorphic settings. While the motivation for classifiers was the feasibility of inference, this was in fact not established. This paper starts with the observation that inference for the full classifier-based system fails. We then identify a subset of the original system for which inference is possible. This subset, which uses implicit classifiers, retains significant expressivity (e.g. it can embed the calculi of Davies and Pfenning) and eliminates the need for classifier names in terms. Implicit classifiers were implemented in MetaOCaml, and no changes were needed to make an existing test suite acceptable by the new type checker. © Springer-Verlag 2004.
|
|
| 4. |
- Duracz, Adam, et al.
(författare)
-
A Semantic Account of Rigorous Simulation
- 2018
-
Ingår i: Principles of Modeling. - Amsterdam : Springer Berlin/Heidelberg. - 9783319952451 - 9783319952468 ; , s. 223-239
-
Bokkapitel (refereegranskat)abstract
- Hybrid systems are a powerful formalism for modeling cyber-physical systems. Reachability analysis is a general method for checking safety properties, especially in the presence of uncertainty and non-determinism. Rigorous simulation is a convenient tool for reachability analysis of hybrid systems. However, to serve as proof tool, a rigorous simulator must be correct w.r.t. a clearly defined notion of reachability, which captures what is intuitively reachable in finite time. As a step towards addressing this challenge, this paper presents a rigorous simulator in the form of an operational semantics and a specification in the form of a denotational semantics. We show that, under certain conditions about the representation of enclosures, the rigorous simulator is correct. We also show that finding a representation satisfying these assumptions is non-trivial. © 2018, Springer International Publishing AG, part of Springer Nature.
|
|
| 5. |
- Moggi, Eugenio, et al.
(författare)
-
An Idealized MetaML : Simpler, and More Expressive
- 1999
-
Ingår i: Programming Languages and Systems. - Berlin : Springer Berlin/Heidelberg. - 3540656995 ; , s. 193-207
-
Konferensbidrag (refereegranskat)abstract
- MetaML is a multi-stage functional programming language featuring three constructs that can be viewed as statically-typed refinements of the back-quote, comma, and eval of Scheme. Thus it provides special support for writing code generators and serves as a semanticallysound basis for systems involving multiple interdependent computational stages. In previous work, we reported on an implementation of MetaML, and on a reduction semantics and type-system for MetaML. In this paper, we present An Idealized MetaML (AIM) that is the result of our study of a categorical model for MetaML. An important outstanding problem is finding a type system that provides the user with a means for manipulating both open and closed code. This problem has eluded efforts by us and other researchers for over three years. AIM solves the issue by providing two type constructors, one classifies closed code and the other open code, and exploiting the way they interact. We point out that AIM can be verbose, and outline a possible remedy relating to the strictness of the closed code type. © Springer International Publishing AG, Part of Springer Science+Business Media 1999
|
|
| 6. |
- Taha, Walid, 1972-, et al.
(författare)
-
Acumen : An Open-source Testbed for Cyber-Physical Systems Research
- 2016
-
Ingår i: Internet of Things. IoT Infrastructures. - Heidelberg : Springer. - 9783319470627 - 9783319470634 ; , s. 118-130
-
Konferensbidrag (refereegranskat)abstract
- Developing Cyber-Physical Systems requires methods and tools to support simulation and verification of hybrid (both continuous and discrete) models. The Acumen modeling and simulation language is an open source testbed for exploring the design space of what rigorous-but-practical next-generation tools can deliver to developers of Cyber-Physical Systems. Like verification tools, a design goal for Acumen is to provide rigorous results. Like simulation tools, it aims to be intuitive, practical, and scalable. However, it is far from evident whether these two goals can be achieved simultaneously.This paper explains the primary design goals for Acumen, the core challenges that must be addressed in order to achieve these goals, the "agile research method" taken by the project, the steps taken to realize these goals, the key lessons learned, and the emerging language design. © ICST Institute for Computer Sciences, Social Informatics and Telecommunications Engineering 2016.
|
|
