programming languages are the way for a person to express a mental plan in a way that the computer can understand. therefore, it is appropriate to consider properties of people when designing new programming languages...
详细信息
programming languages are the way for a person to express a mental plan in a way that the computer can understand. therefore, it is appropriate to consider properties of people when designing new programming languages. In our research, we are investigating how people think about algorithms, and how programming languages can be made easier to learn and more effective for people to use. By taking human-productivity aspects of programming languages seriously, designers can more effectively match programming language features with human capabilities and problem solving methods. Human factors methods can be used to measure the effects, so unsubstantiated claims can be avoided. this talk will present a quick summary of new and old results in what is known about people and programming;from areas that are sometimes called "empirical studies of programmers" and "psychology of programming." Much is known about what people find difficult, and what syntax and language features are especially tricky and bug-prone. Our new research has discovered how people naturally think about algorithms and data structures, which can help with making programming languages more closely match people's problem solving techniques.
this paper presents a methodology for implementing natural language morphology in the functional language Haskell. the main idea behind is simple: instead of working with untyped regular expressions, which is the stat...
详细信息
this paper presents a methodology for implementing natural language morphology in the functional language Haskell. the main idea behind is simple: instead of working with untyped regular expressions, which is the state of the art of morphology in computational linguistics, we use finite functions over hereditarily finite algebraic datatypes. the definitions of these datatypes and functions are the language-dependent part of the morphology. the language-independent part consists of an untyped dictionary format which is used for synthesis of word forms, and a decorated trie, which is used for analysis. functional Morphology builds on ideas introduced by Huet in his computational linguistics toolkit Zen, which he has used to implement the morphology of Sanskrit. the goal has been to make it easy for linguists, who are not trained as functional programmers, to apply the ideas to new languages. As a proof of the productivity of the method, morphologies for Swedish, Italian, Russian, Spanish, and Latin have already been implemented using the library. the Latin morphology is used as a running example in this article.
We describe the Funlogic system which extends a functional language with existentially quantified declarations. An existential declaration introduces a variable and a set of constraints that its value should meet. Exi...
详细信息
functional Reactive programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals. FRP is based on the synchronous data-flow paradigm and supports ...
详细信息
ISBN:
(纸本)9781605583327
functional Reactive programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals. FRP is based on the synchronous data-flow paradigm and supports both continuous-time and discrete-time signals (hybrid systems). What sets FRP apart from Most other languages for similar applications is its support for systems with dynamic structure and for higher-order reactive constructs. Statically guaranteeing correctness properties of programs is an attractive proposition. this is true in particular for typical application domains for reactive programming such as embedded systems. To that end, many existing reactive languages have type systems or other static checks that guarantee domain-specific properties, such as feedback loops always being well-formed. However, they are limited in their capabilities to support dynamism and higher-order data-flow compared with FRP. thus, the onus of ensuring such properties of FRP programs has so far been on the programmer as established static techniques do not suffice. In this paper, we show how dependent types allow this concern to be addressed. We present an implementation of FRP embedded in the dependently-typed language Agda, leveraging the type system of the host language to craft a domain-specific (dependent) type system for FRP. the implementation constitutes a discrete, operational semantics of FRP, and as it passes the Agda type, coverage, and termination checks, we know the operational semantics is total, which means our type system is safe.
We present a compositional programme logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters. return values, con...
详细信息
ISBN:
(纸本)9781595930644
We present a compositional programme logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters. return values, content of references and parts of data structures. the programme logic extends our earlier logic for alias-free imperative higher-order functions with new operators which serve as building blocks for clean structural reasoning about programms and data structures in the presence of aliasing. this has been an open issue since the pioneering work by Cartwright-Oppen and Morris twenty-five years ago. We illustrate usage of the logic for description and reasoning through concrete examples including a higher-order polymorphic Quicksort. the logical status of the new operators is clarified by translating them into (in)equalities of reference names.
We describe an experimental attempt at verification of Smalltalk VM using mechanized proof. Only the native code generation part is verified. the generator is developed in the Coq proof assistant and is largely based ...
详细信息
Many useful programming constructions can be expressed as monads. Examples include probabilistic modeling, functional reactive programming, parsing, and information flow tracking, not to mention effectful functionalit...
详细信息
ISBN:
(纸本)9781450308656
Many useful programming constructions can be expressed as monads. Examples include probabilistic modeling, functional reactive programming, parsing, and information flow tracking, not to mention effectful functionality like state and I/O. In this paper, we present a type-based rewriting algorithm to make programming with arbitrary monads as easy as using ML's built-in support for state and I/O. Developers write programs using monadic values of type m T as if they were of type T, and our algorithm inserts the necessary binds, units, and monad-to-monad morphisms so that the program type checks. Our algorithm, based on Jones' qualified types, produces principal types. But principal types are sometimes problematic: the program's semantics could depend on the choice of instantiation when more than one instantiation is valid. In such situations we are able to simplify the types to remove any ambiguity but without adversely affecting typability;thus we can accept strictly more programs. Moreover, we have proved that this simplification is efficient (linear in the number of constraints) and coherent: while our algorithm induces a particular rewriting, all related rewritings will have the same semantics. We have implemented our approach for a core functional language and applied it successfully to simple examples from the domains listed above, which are used as illustrations throughout the paper.
It is possible to extend the basic notion of "function call" to allow functions to have multiple return points. this turns out to be a surprisingly useful mechanism. this article conducts a fairly wide-rangi...
详细信息
It is possible to extend the basic notion of "function call" to allow functions to have multiple return points. this turns out to be a surprisingly useful mechanism. this article conducts a fairly wide-ranging tour of such a feature: a formal semantics for a minimal A-calculus capturing the mechanism;motivating examples;monomorphic and parametrically polymorphic static type systems;useful transformations;implementation concerns and experience with an implementation;and comparison to related mechanisms, such as exceptions, sum-types and explicit continuations. We conclude that multiple-return function call is not only a useful and expressive mechanism, at boththe source-code and intermediate-representation levels, but also quite inexpensive to implement.
Information Flow Control (IFC) in dynamic contexts is challenging due to different interpretations of security that arise. this paper introduces a modular framework to address this challenge. We present a dynamic floa...
详细信息
ISBN:
(纸本)9798400703843
Information Flow Control (IFC) in dynamic contexts is challenging due to different interpretations of security that arise. this paper introduces a modular framework to address this challenge. We present a dynamic floating-label enforcement mechanism that can be instantiated based on the intended security. Our approach formalizes a simply typed lambda-calculus, extended with IFC operations, and adopts an epistemic perspective on security definition.
the Object Management Group's (OMG) Data Distribution Service (DDS) provides many configurable policies which determine end-to-end quality of service (QoS) of applications. It is challenging to predict the system&...
详细信息
ISBN:
(纸本)9781450323734
the Object Management Group's (OMG) Data Distribution Service (DDS) provides many configurable policies which determine end-to-end quality of service (QoS) of applications. It is challenging to predict the system's performance in terms of latencies, throughput, and resource usage because diverse combinations of QoS configurations influence QoS of applications in different ways. To overcome this problem, design-time formal methods have been applied with mixed success, but lack of sufficient accuracy in prediction, tool support, and understanding of formalism has prevented wider adoption of the formal techniques. A promising approach to address this challenge is to emulate system behavior and gather data on the QoS parameters of interest by experimentation. To realize this approach, which is preferred over formal methods due to their limitations in accurately predicting QoS, we have developed a model-based automatic performance testing framework with generative capabilities to reduce manual efforts in generating a large number of relevant QoS configurations that can be deployed and tested on a cloud platform. this paper describes our initial efforts in developing and using this technology.
暂无评论