Demo Data from SIGIR 2026 / reviewers in the wild / expert
Paul Hudak
dblp:h/PaulHudak
· DBLP profile ↗
49ranked-venue papers
14as first author
0since 2021 · last 2014
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 39 · 11 first-authorSystems, architecture and hardware · 7 · 3 first-authorArtificial intelligence and machine learning · 1Computer networks · 1Theory of computation · 1Applied, interdisciplinary, general and emerging computing · 1
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Software engineering, system software, and programming languages
18 papers |
Programming languages and type systems · 80% Compilers and program optimization · 9% Program analysis · 9% | |
| Computer networks
1 paper |
Software-defined and programmable networks · 100% | |
| Computer architecture, parallel and distributed computing, and storage systems
8 papers |
Parallel and multicore computing · 68% Memory systems · 19% Embedded and real-time systems · 6% |
Topics — the 30 heaviest of 63, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Software-defined and programmable networks
SDN controller |
0.2 | 1 | 2013 | Maple: simplifying SDN programming using algorithmic policies · SIGCOMM 2013 |
Software-defined and programmable networks › network programming
SDN programming |
0.2 | 1 | 2013 | Maple: simplifying SDN programming using algorithmic policies · SIGCOMM 2013 |
Programming languages and type systems › computational effects
monads |
0.1 | 3 | 2004 | First-class monadic schedules · ACM Trans. Program. Lang. Syst. 2004 Rolling Your Own MADT - A Connection Between Linear Types and Monads · POPL 1997 Monad Transformers and Modular Interpreters · POPL 1995 |
Parallel and multicore computing › parallel computing › parallel programming languages
parallel functional programming |
0.1 | 2 | 2004 | First-class monadic schedules · ACM Trans. Program. Lang. Syst. 2004 Para-Functional Programming: A Paradigm for Programming Multiprocessor Systems · POPL 1986 |
Software-defined and programmable networks
programmable data plane |
0.0 | 1 | 2013 | Maple: simplifying SDN programming using algorithmic policies · SIGCOMM 2013 |
Programming languages and type systems
domain-specific languages |
0.0 | 2 | 1999 | Prototyping Real-Time Vision Systems: An Experiment in DSL Design · ICSE 1999 A Language for Declarative Robotic Programming · ICRA 1999 |
Programming languages and type systems
functional programming |
0.0 | 5 | 1999 | Prototyping Real-Time Vision Systems: An Experiment in DSL Design · ICSE 1999 A Language for Declarative Robotic Programming · ICRA 1999 Single-Threaded Polymorphic Lambda Calculus · LICS 1990 |
Programming languages and type systems › language semantics › formal semantics
operational semantics |
0.0 | 2 | 1997 | Rolling Your Own MADT - A Connection Between Linear Types and Monads · POPL 1997 Call by Name, Assignment, and the Lambda Calculus · POPL 1993 |
Programming languages and type systems › programming paradigms
functional reactive programming |
0.0 | 1 | 2000 | Functional reactive programming from first principles · PLDI 2000 |
Image and video processing
real-time vision |
0.0 | 1 | 1999 | Prototyping Real-Time Vision Systems: An Experiment in DSL Design · ICSE 1999 |
Programming languages and type systems › domain-specific languages
embedded domain-specific languages |
0.0 | 1 | 1999 | Prototyping Real-Time Vision Systems: An Experiment in DSL Design · ICSE 1999 |
Programming languages and type systems › domain-specific languages
robot programming languages |
0.0 | 1 | 1999 | A Language for Declarative Robotic Programming · ICRA 1999 |
Programming languages and type systems › language semantics
graph rewriting semantics |
0.0 | 1 | 1997 | Rolling Your Own MADT - A Connection Between Linear Types and Monads · POPL 1997 |
Programming languages and type systems › type systems › substructural type systems
linear types |
0.0 | 1 | 1997 | Rolling Your Own MADT - A Connection Between Linear Types and Monads · POPL 1997 |
Programming languages and type systems
type systems |
0.0 | 1 | 1997 | Rolling Your Own MADT - A Connection Between Linear Types and Monads · POPL 1997 |
Parallel and multicore computing
parallel programming models |
0.0 | 2 | 2004 | First-class monadic schedules · ACM Trans. Program. Lang. Syst. 2004 Distributed Execution of Functional Programs Using Serial Combinators · IEEE Trans. Computers 1985 |
Programming languages and type systems
lambda calculus |
0.0 | 2 | 1993 | Call by Name, Assignment, and the Lambda Calculus · POPL 1993 Higher-Order Strictness Analysis in Untyped Lambda Calculus · POPL 1986 |
Parallel and multicore computing › parallel programming models
futures |
0.0 | 1 | 2004 | First-class monadic schedules · ACM Trans. Program. Lang. Syst. 2004 |
Programming languages and type systems
computational effects |
0.0 | 1 | 1995 | Monad Transformers and Modular Interpreters · POPL 1995 |
Programming languages and type systems › computational effects
monad transformers |
0.0 | 1 | 1995 | Monad Transformers and Modular Interpreters · POPL 1995 |
Program analysis › static analysis
abstract interpretation |
0.0 | 2 | 1991 | Collecting Interpretations of Expressions · ACM Trans. Program. Lang. Syst. 1991 A Collecting Interpretation of Expressions (Without Powerdomains) · POPL 1988 |
Program analysis › static analysis › abstract interpretation
strictness analysis |
0.0 | 2 | 1991 | Collecting Interpretations of Expressions · ACM Trans. Program. Lang. Syst. 1991 Higher-Order Strictness Analysis in Untyped Lambda Calculus · POPL 1986 |
Programming languages and type systems › term rewriting
confluence |
0.0 | 1 | 1993 | Call by Name, Assignment, and the Lambda Calculus · POPL 1993 |
Memory systems
cache coherence |
0.0 | 2 | 1989 | Memory Coherence in Shared Virtual Memory Systems · ACM Trans. Comput. Syst. 1989 Memory Coherence in Shared Virtual Memory Systems · PODC 1986 |
Memory systems › virtual memory management
shared virtual memory |
0.0 | 2 | 1989 | Memory Coherence in Shared Virtual Memory Systems · ACM Trans. Comput. Syst. 1989 Memory Coherence in Shared Virtual Memory Systems · PODC 1986 |
Programming languages and type systems › language semantics › formal semantics
denotational semantics |
0.0 | 3 | 1991 | A Collecting Interpretation of Expressions (Without Powerdomains) · POPL 1988 Collecting Interpretations of Expressions · ACM Trans. Program. Lang. Syst. 1991 Realistic Compilation by Program Transformation · POPL 1989 |
Embedded and real-time systems › cyber-physical system platforms
hybrid systems |
0.0 | 1 | 2000 | Functional reactive programming from first principles · PLDI 2000 |
Program analysis
data flow analysis |
0.0 | 1 | 1991 | Collecting Interpretations of Expressions · ACM Trans. Program. Lang. Syst. 1991 |
Programming languages and type systems › language semantics
formal semantics |
0.0 | 1 | 1991 | Monitoring Semantics: A Formal Framework for Specifying, Implementing, and Reasoning about Execution Monitors · PLDI 1991 |
Program analysis › static analysis
incremental analysis |
0.0 | 1 | 1991 | Incremental Compilation via Partial Evaluation · POPL 1991 |
Methods — techniques the papers use, named apart from their topics
tracing runtime optimization · 0.2policy decision caching · 0.2dependency tracing · 0.2barnes-hut method · 0.1algebraic properties · 0.1domain-specific language · 0.1behaviors and events · 0.1haskell · 0.0functional programming · 0.0domain-specific language design · 0.0domain-specific embedded language · 0.0correctness proof · 0.0CPS translation · 0.0simulation · 0.0distributed coherence algorithm · 0.0centralized coherence algorithm · 0.0coherence protocol design · 0.0program transformation · 0.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2014 | Settable and non-interfering signal functions for FRP: how a first-order switch is more than enoughabstractFunctional Reactive Programming (FRP) provides a method for programming continuous, reactive systems by utilizing signal functions that, abstractly, transform continuous input signals into continuous output signals. These signals may also be streams of events, and indeed, by allowing signal functions themselves to be the values carried by these events (in essence, signals of signal functions), one can conveniently make discrete changes in program behavior by "switching" into and out of these signal functions. This higher-order notion of switching is common among many FRP systems, in particular those based on arrows, such as Yampa. Daniel Winograd-Cort, Paul Hudak |
ICFP | 2 |
| 2013 | Mio: a high-performance multicore io manager for GHCabstractHaskell threads provide a key, lightweight concurrency abstraction to simplify the programming of important network applications such as web servers and software-defined network (SDN) controllers. The flagship Glasgow Haskell Compiler (GHC) introduces a run-time system (RTS) to achieve a high-performance multicore implementation of Haskell threads, by introducing effective components such as a multicore scheduler, a parallel garbage collector, an IO manager, and efficient multicore memory allocation. Evaluations of the GHC RTS, however, show that it does not scale well on multicore processors, leading to poor performance of many network applications that try to use lightweight Haskell threads. In this paper, we show that the GHC IO manager, which is a crucial component of the GHC RTS, is the scaling bottleneck. Through a series of experiments, we identify key data structure, scheduling, and dispatching bottlenecks of the GHC IO manager. We then design a new multicore IO manager named Mio that eliminates all these bottlenecks. Our evaluations show that the new Mio manager improves realistic web server throughput by 6.5x and reduces expected web server response time by 5.7x. We also show that with Mio, McNettle (an SDN controller written in Haskell) can scale effectively to 40+ cores, reach a throughput of over 20 million new requests per second on a single machine, and hence become the fastest of all existing SDN controllers. Andreas Voellmy, Junchang Wang, Paul Hudak, Kazuhiko Yamamoto |
Haskell | 3 |
| 2013 | Maple: simplifying SDN programming using algorithmic policiesabstractSoftware-Defined Networking offers the appeal of a simple, centralized programming model for managing complex networks. However, challenges in managing low-level details, such as setting up and maintaining correct and efficient forwarding tables on distributed switches, often compromise this conceptual simplicity. In this pa- per, we present Maple, a system that simplifies SDN programming by (1) allowing a programmer to use a standard programming language to design an arbitrary, centralized algorithm, which we call an algorithmic policy, to decide the behaviors of an entire network, and (2) providing an abstraction that the programmer-defined, centralized policy runs, conceptually, "afresh" on every packet entering a network, and hence is oblivious to the challenge of translating a high-level policy into sets of rules on distributed individual switches. To implement algorithmic policies efficiently, Maple includes not only a highly-efficient multicore scheduler that can scale efficiently to controllers with 40+ cores, but more importantly a novel tracing runtime optimizer that can automatically record reusable policy decisions, offload work to switches when possible, and keep switch flow tables up-to-date by dynamically tracing the dependency of policy decisions on packet contents as well as the environment (system state). Evaluations using real HP switches show that Maple optimizer reduces HTTP connection time by a factor of 100 at high load. During simulated benchmarking, Maple scheduler, when not running the optimizer, achieves a throughput of over 20 million new flow requests per second on a single machine, with 95-percentile latency under 10 ms. Andreas Voellmy, Junchang Wang, Yang Richard Yang, Bryan Ford, Paul Hudak |
SIGCOMM | 5 |
| 2012 | Wormholes: introducing effects to FRPabstractFunctional reactive programming (FRP) is a useful model for programming real-time and reactive systems in which one defines a signal function to process a stream of input values into a stream of output values. However, performing side effects (e.g. memory mutation or input/output) in this model is tricky and typically unsafe. In previous work, Winograd-Cort et al. [2012] introduced resource types and wormholes to address this problem. Daniel Winograd-Cort, Paul Hudak |
Haskell | 2 |
| 2012 | Virtualizing Real-World Objects in FRP
Daniel Winograd-Cort, Hai Liu 0012, Paul Hudak |
PADL | 3 |
| 2011 | Nettle: Taking the Sting Out of Programming Network Routers
Andreas Voellmy, Paul Hudak |
PADL | 2 |
| 2011 | Causal commutative arrowsabstractAbstract Arrows are a popular form of abstract computation. Being more general than monads, they are more broadly applicable, and, in particular, are a good abstraction for signal processing and dataflow computations. Most notably, arrows form the basis for a domain-specific language called Yampa , which has been used in a variety of concrete applications, including animation, robotics, sound synthesis, control systems, and graphical user interfaces. Our primary interest is in better understanding the class of abstract computations captured by Yampa. Unfortunately, arrows are not concrete enough to do this with precision. To remedy this situation, we introduce the concept of commutative arrows that capture a noninterference property of concurrent computations. We also add an init operator that captures the causal nature of arrow effects, and identify its associated law. To study this class of computations in more detail, we define an extension to arrows called causal commutative arrows (CCA), and study its properties. Our key contribution is the identification of a normal form for CCA called causal commutative normal form (CCNF). By defining a normalization procedure, we have developed an optimization strategy that yields dramatic improvements in performance over conventional implementations of arrows. We have implemented this technique in Haskell, and conducted benchmarks that validate the effectiveness of our approach. When compiled with the Glasgow Haskell Compiler (GHC), the overall methodology can result in significant speedups. Hai Liu 0012, Eric Cheng, Paul Hudak |
J. Funct. Program. | 3 |
| 2010 | An Ode to Arrows
Hai Liu 0012, Paul Hudak |
PADL | 2 |
| 2009 | Causal commutative arrows and their optimizationabstractArrows are a popular form of abstract computation. Being more general than monads, they are more broadly applicable, and in particular are a good abstraction for signal processing and dataflow computations. Most notably, arrows form the basis for a domain specific language called Yampa, which has been used in a variety of concrete applications, including animation, robotics, sound synthesis, control systems, and graphical user interfaces. Our primary interest is in better understanding the class of abstract computations captured by Yampa. Unfortunately, arrows are not concrete enough to do this with precision. To remedy this situation we introduce the concept of commutative arrows that capture a kind of non-interference property of concurrent computations. We also add an init operator, and identify a crucial law that captures the causal nature of arrow effects. We call the resulting computational model causal commutative arrows. To study this class of computations in more detail, we define an extension to the simply typed lambda calculus called causal commutative arrows (CCA), and study its properties. Our key contribution is the identification of a normal form for CCA called causal commutative normal form (CCNF). By defining a normalization procedure we have developed an optimization strategy that yields dramatic improvements in performance over conventional implementations of arrows. We have implemented this technique in Haskell, and conducted benchmarks that validate the effectiveness of our approach. When combined with stream fusion, the overall methodology can result in speed-ups of greater than two orders of magnitude. Hai Liu 0012, Eric Cheng, Paul Hudak |
ICFP | 3 |
| 2007 | HPorter: Using Arrows to Compose Parallel Processes
Liwen Huang, Paul Hudak, John Peterson |
PADL | 2 |
| 2004 | An Algebraic Theory of Polymorphic Temporal Media
Paul Hudak |
PADL | 1 |
| 2004 | EditorialabstractThis issue of the Journal of Functional Programming marks a point of transition. Our long-time Chief Editors, Simon Peyton Jones and Philip Wadler, are stepping down. Most of us are aware of the amazing research contributions that Simon and Phil have made to functional programming. But you may not be aware how much these two have put in behind the scenes. Paul Hudak, J. Gregory Morrisett |
J. Funct. Program. | 1 |
| 2004 | First-class monadic schedulesabstractParallel functional languages often use meta-linguistic annotations to provide control over parallel evaluation. In this paper we explore a flexible mechanism to control when an expression is evaluated: first-class monadic schedules . We discuss the advantages of using such first-class values over traditional annotation-based systems. In particular, it is often desirable to make decisions about the operational behavior of parallel programs depending on the dynamic state of the system. For example, we may want to measure the system load before deciding to evaluate expressions in parallel. For this purpose, we show how monads can be used to access dynamic system parameters in a referentially transparent manner (up to termination).As a mechanism to reason about schedules, we present a set of algebraic properties that any implementation of schedules must satisfy. We also describe an implementation that translates schedules into a dialect of Scheme extended with futures . We prove that this implementation satisfies the given set of algebraic properties, and give performance results for a parallel solution to the n -body problem using the Barnes--Hut method.Although our ideas were developed specifically for nonstrict functional languages such as Haskell, we briefly discuss how they can be used with strict functional languages and imperative languages as well. Rajiv Mirani, Paul Hudak |
ACM Trans. Program. Lang. Syst. | 2 |
| 2003 | Functional Hybrid Modeling
Henrik Nilsson, John Peterson, Paul Hudak |
PADL | 3 |
| 2002 | Event-Driven FRP
Zhanyong Wan, Walid Taha, Paul Hudak |
PADL | 3 |
| 2001 | Real-Time FRPabstractFunctional reactive programming (FRP) is a declarative programming paradigm where the basic notions are continuous, time-varying behaviors and discrete, event-based reactivity. FRP has been used successfully in many reactive programming domains such as animation, robotics, and graphical user interfaces. The success of FRP in these domains encourages us to consider its use in real-time applications, where it is crucial that the cost of running a program be bounded and known before run-time. But previous work on the semantics and implementation of FRP was not explicitly concerned about the issues of cost. In fact, the resource consumption of FRP programs in the current implementation is often hard to predict. As a first step towards addressing these concerns, this paper presents real-time FRP (RT-FRP), a statically-typed language where the time and space cost of each execution step for a given program is statically bounded. To take advantage of existing work on languages with bounded resources, we split RT-FRP into two parts: a reactive part that captures the essential ingredients of FRP programs, and a base language part that can be instantiated to any generic programming language that has been shown to be terminating and resource-bounded. This allows us to focus on the issues specific to RT-FRP, namely, two forms of recursion. After presenting the operational explanation of what can go wrong due to the presence of recursion, we show how the typed version of the language is terminating and resource-bounded. Most of our FRP programs are expressible directly in RT. The rest are expressible via a simple mechanism that integrates RT-FRP with the base language. Zhanyong Wan, Walid Taha, Paul Hudak |
ICFP | 3 |
| 2001 | FVision: A Declarative Language for Visual Tracking
John Peterson, Paul Hudak, Alastair Reid 0001, Gregory D. Hager |
PADL | 2 |
| 2000 | Functional reactive programming from first principlesabstractFunctional Reactive Programming, or FRP, is a general framework for programming hybrid systems in a high-level, declarative manner. The key ideas in FRP are its notions of behaviors and events. Behaviors are time-varying, reactive values, while events are time-ordered sequences of discrete-time event occurrences. FRP is the essence of Fran, a domain-specific language embedded in Haskell for programming reactive animations, but FRP is now also being used in vision, robotics and other control systems applications. Zhanyong Wan, Paul Hudak |
PLDI | 2 |
| 1999 | Functional Reactive Programming (Abstract)
Paul Hudak |
ESOP | 1 |
| 1999 | A Language for Declarative Robotic ProgrammingabstractWe have applied methodologies developed for domain-specific embedded languages to create a high-level robot control language called Frob, for functional robotics. Frob supports a programming style that cleanly separates the what from the how of a robotic control program. That is, the what is a simple, easily understood definition of the control strategy using groups of equations and primitives which combine sets of these control system equations into a complex system. The how aspect of the program addresses the unpleasant details, such as the method used to realize these equations, the connection between the control equations and the sensors and effectors in the robot, and communication with other elements of the system. Frob is a system that supports rapid prototyping of new control strategies, enables software reuse through composition, and defines a system in a way that can be formally reasoned about and transformed. John Peterson, Gregory D. Hager, Paul Hudak |
ICRA | 3 |
| 1999 | Prototyping Real-Time Vision Systems: An Experiment in DSL DesignabstractDescribes the enhancement of XVision, a large library of C++ code for real-time vision processing, into FVision (pronounced fission), a fully-featured domain-specific language (DSL) embedded in Haskell. The resulting prototype system substantiates the claims of increased modularity, effective code reuse and rapid prototyping that characterize the DSL approach to systems design. It also illustrates the need for judicious interface design: relegating computationally expensive tasks to XVision (pre-existing C++ components) and leaving modular compositional tasks to FVision (Haskell). At the same time, our experience demonstrates how Haskell's advanced language features (specifically, parametric polymorphism, lazy evaluation, higher-order functions and automatic storage reclamation) permit a rapid DSL design that is itself highly modular and easily modified. Overall, the resulting hybrid system exceeded our expectations: visual tracking programs continue to spend most of their time executing low-level image processing code, while Haskell's advanced features allow us to quickly develop and test small prototype systems within a matter of a few days, and to develop realistic applications within a few weeks. Alastair Reid 0001, John Peterson, Gregory D. Hager, Paul Hudak |
ICSE | 4 |
| 1999 | Shifting Expression Procedures into Reverse
Mark Tullsen, Paul Hudak |
PEPM | 2 |
| 1998 | Modular domain specific languages and toolsabstractA domain specific language (DSL) allows one to develop software for a particular application domain quickly and effectively, yielding programs that are easy to understand, reason about, and maintain. On the other hand, there may be a significant overhead in creating the infrastructure needed to support a DSL. To solve this problem, a methodology is described for building domain specific embedded languages (DSELs), in which a DSL is designed within an existing, higher-order and typed, programming language such as Haskell or ML. In addition, techniques are described for building modular interpreters and tools for DSELs. The resulting methodology facilitates reuse of syntax semantics, implementation code, software tools, as well as look-and-feel. Paul Hudak |
ICSR | 1 |
| 1997 | Functional Reactive AnimationabstractFran (Functional Reactive Animation) is a collection of data types and functions for composing richly interactive, multi-media animations. The key ideas in Fran are its notions of behaviors and events. Behaviors are time-varying, reactive values, while events are sets of arbitrarily complex condi-tions, carrying possibly rich information. Most traditional values can be treated as behaviors, and when images are thus treated, they become animations. Although these no-tions are captured as data types rather than a programming language, we provide them with a denotational semantics, including a proper treatment of real time, to guide reason-ing and implementation. A method to eectively and ef-ciently perform event detection using interval analysis is also described, which relies on the partial information struc-ture on the domain of event times. Fran has been imple-mented in Hugs, yielding surprisingly good performance for an interpreter-based system. Several examples are given, in-cluding the ability to describe physical phenomena involving Conal Elliott, Paul Hudak |
ICFP | 2 |
| 1997 | Rolling Your Own MADT - A Connection Between Linear Types and MonadsabstractA methodology is described whereby a linear ADT may be rigorously encapsulated within a state monad. A CPS-like translation from the original ADT axioms into monadic ones is also described and proven correct, so that reasoning can be accomplished at the monadic level without exposing the state. The ADT axioms are suitably constrained by a linear type system to make this translation possible. This constraint also allows the state to be "updated in place," a notion made precise via a graph-rewrite operational semantics. 1 Introduction In recent years, numerous proposals for I/O, destructive updates to data structures, mutable variables, nondeterminism, and concurrency have been put forth, all using monads to structure programs in such a way that details of the computation are effectively hidden and encapsulated [18, 20]. One of the most important uses of monads is in dealing with state, resulting in a style of programming referred to appropriately by Peyton Jones and Wadler as imperativ... Chih-Ping Chen, Paul Hudak |
POPL | 2 |
| 1996 | Modular Denotational Semantics for Compiler Construction
Sheng Liang, Paul Hudak |
ESOP | 2 |
| 1996 | Haskore Music Notation - An Algebra of MusicabstractAbstract We have developed a simple algebraic approach to music description and composition called Haskore . In this framework, musical objects consist of primitive notions such as notes and rests, operations to transform musical objects such as transpose and tempo-scaling, and operations to combine musical objects to form more complex ones, such as concurrent and sequential composition. When these simple notions are embedded into a functional language such as Haskell, rather complex musical relationships can be expressed clearly and succinctly. Exploiting the algebraic properties of Haskore, we have further defined a notion of literal performance (devoid of articulation) through which observationally equivalent musical objects can be determined. With this basis many useful properties can be proved, such as commutative, associative, and distributive properties of various operators. An algebra of music thus surfaces. Paul Hudak, Tom Makucevich, Syam Gadde, Bo Whong |
J. Funct. Program. | 1 |
| 1995 | Monad Transformers and Modular InterpretersabstractWe show how a set of building blocks can be used to construct programming language interpreters, and present implementations of such building blocks capable of supporting many commonly known features, including simple expressions, three different function call mechanisms (call-by-name, call-by-value and lazy evaluation), references and assignment, nondeterminism, first-class continuations, and program tracing. Sheng Liang, Paul Hudak, Mark P. Jones |
POPL | 2 |
| 1995 | Semantics Directed Program Execution MonitoringabstractAbstract Monitoring semantics is a formal model of program execution which captures ‘monitoring activity’ as found in profilers, tracers, debuggers, etc. Beyond its theoretical interest, this formalism provides a new methodology for implementing a large family of source-level monitoring activities for sequential deterministic programming languages. In this article we explore the use of monitoring semantics in the specification and implementation of a variety of monitors: profilers, tracers, collecting interpreters, and, most importantly, interactive source-level debuggers. Although we consider such monitors only for (both strict and non-strict) functional languages, the methodology extends easily to imperative languages, since it begins with a continuation semantics specification. In addition, using standard partial evaluation techniques as an optimization strategy, we show that the methodology forms a practical basis for building real monitors. Our system can be optimized at two levels of specialization: specializing the interpreter with respect to a monitor specification automatically yields an instrumented interpreter; further specializing this instrumented interpreter with respect to a source program yields an instrumented program, i.e. one in which the extra code to perform monitoring has been automatically embedded into the program. Amir Kishon, Paul Hudak |
J. Funct. Program. | 2 |
| 1993 | Call by Name, Assignment, and the Lambda CalculusabstractWe define an extension of the call-by-name lambda calculus with additional constructs and reduction rules that represent mutable variables and assignments. The extended calculus has neither a concept of an explicit store nor a concept of evaluation order; nevertheless, we show that programs in the calculus can be implemented using a single-threaded store. We also show that the new calculus has the Church-Rosser property and that it is a conservative extension of classical lambda calculus with respect to operational equivalence; that is, all algebraic laws of the functional subset are preserved. Martin Odersky, Dan Rabin, Paul Hudak |
POPL | 3 |
| 1991 | Monitoring Semantics: A Formal Framework for Specifying, Implementing, and Reasoning about Execution MonitorsabstractWe introduce monitoring semantics, a non-standard model Amir Kishon, Paul Hudak, Charles Consel |
PLDI | 2 |
| 1991 | Incremental Compilation via Partial EvaluationabstractArticle A theory of incremental computation and its application Share on Authors: R. S. Sundaresh Yale University, Department of Computer Science, Box 2158 Yale Station, New Haven, CT Yale University, Department of Computer Science, Box 2158 Yale Station, New Haven, CTView Profile , Paul Hudak Yale University, Department of Computer Science, Box 2158 Yale Station, New Haven, CT Yale University, Department of Computer Science, Box 2158 Yale Station, New Haven, CTView Profile Authors Info & Claims POPL '91: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1991 Pages 1–13https://doi.org/10.1145/99583.99587Online:03 January 1991Publication History 22citation447DownloadsMetricsTotal Citations22Total Downloads447Last 12 Months7Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access R. S. Sundaresh, Paul Hudak |
POPL | 2 |
| 1991 | Collecting Interpretations of ExpressionsabstractA collecting interpretation of expressions is an interpretation of a program that allows one to answer questions of the sort: “What are all possible values to which an expression might evaluate during program execution?” Answering such questions in a denotational framework is akin to traditional data flow analysis and, when used in the context of abstract interpretation, allows one to infer properties that approximate the run-time behavior of expression evaluation. Exact collecting interpretations of expressions are developed for three abstract functional languages: a strict first-order language, a nonstrict first-order language, and a nonstrict higher order language (the full untyped lambda calculus with constants). It is argued that the method is simple (in particular, no powerdomains are needed), Natural (it captures the intuitive operational behavior of a cache), yet more expressive than existing methods (it is the first exact collecting interpretation for either nonstrict higher order languages). Correctness of the interpretations with respect to the standard semantics is shown via a generalization of the notion of strictness. It is further shown how to form abstractions of these exact interpretations, using as an example a collecting strictness analysis which yields compile-time information not previously captured by conventional strictness analyses. Paul Hudak |
ACM Trans. Program. Lang. Syst. | 1 |
| 1990 | Single-Threaded Polymorphic Lambda CalculusabstractThe primary goal of this study is to devise a method to express mutations to state in a modern (higher order, polymorphic, nonstrict) functional language, without sacrificing referential transparency, and with a simple, easy-to-reason-about semantics. Although collectively these properties seem contradictory, a satisfactory solution is found. Aside from the fundamental property of referential transparency, the two key properties that the authors maximize are simplicity and expressiveness. The system must be easy to use: expressing mutations to state should be natural, and the resulting behavior should be easy to reason about.> Juan C. Guzmán, Paul Hudak |
LICS | 2 |
| 1990 | Compilation of Haskell Array Comprehensions for Scientific ComputingabstractMonolithic approaches to functional language arrays, such as Haskell array comprehensions, define elements all at once, at the time the array is created, instead of incrementally. Although monolithic arrays are elegant, a naive implementation can be very inefficient. For example, if a compiler does not know whether an element has zero or many definitions, it must compile runtime tests. If a compiler does not know inter-element data dependencies, it must resort to pessimistic strategies such as compiling elements as thunks, or making unnecessary copies when updating an array. Steven Anderson, Paul Hudak |
PLDI | 2 |
| 1989 | Realistic Compilation by Program TransformationabstractUsing concepts from denotational semantics, we have produced a very simple compiler that can be used to compile standard programming languages and produces object code as efficient as that of production compilers. The compiler is based entirely on source-to-source transformations performed on programs that have been translated into an intermediate language resembling the lambda calculus. The output of the compiler, while still in the intermediate language, can be trivially translated into machine code for the target machine. The compilation by transformation strategy is simple: the goal is to remove any dependencies on the intermediate language semantics that the target machine cannot implement directly. Front-ends have been written for Pascal, BASIC, and Scheme and the compiler produces code for the MC68020 microprocessor. Richard Kelsey, Paul Hudak |
POPL | 2 |
| 1989 | An Optimising Compiler for a Modern Functional LanguageabstractOne of the factor hindering the use of functional languages has been their relatively poor performance in comparison to more traditional languages such as C and Pascal. During the last decade tremendous progress has been made in building implementations of functional languages but the approaches adopted have employed specialist hardware and/or compiler optimisations that have been developed specifically for functional languages. Building specialist hardware may be the best long-term solution but in the short run it is possible to increase the use and acceptance of functional languages by exploiting the performance of commercially available machines. The goal of the project described in this paper has been to design an optimising compiler that produces fast code for functional languages on conventional sequential and parallel machines. Adrienne G. Bloss, Paul Hudak |
Comput. J. | 2 |
| 1989 | Memory Coherence in Shared Virtual Memory SystemsabstractThe memory coherence problem in designing and implementing a shared virtual memory on loosely coupled multiprocessors is studied in depth. Two classes of algorithms, centralized and distributed, for solving the problem are presented. A prototype shared virtual memory on an Apollo ring based on these algorithms has been implemented. Both theoretical and practical results show that the memory coherence problem can indeed be solved efficiently on a loosely coupled multiprocessor. Kai Li 0001, Paul Hudak |
ACM Trans. Comput. Syst. | 2 |
| 1988 | A Collecting Interpretation of Expressions (Without Powerdomains)abstractA collecting interpretation of expressions is an interpretation of a program that allows one to answer questions of the sort: “What are all possible values to which an expression might evaluate during program execution?” Answering such questions in a denotational framework is akin to traditional data flow analysis, and when used in the context of abstract interpretation allows one to infer properties that approximate the run-time behavior of expression evaluation. In this paper collecting interpretations of expressions are developed for three abstract functional languages: (1) a first-order language with call-by-value semantics, (2) a first-order language with call-by-name semantics, and (3) a higher-order language with call-by-name semantics (i.e., the full untyped lambda calculus with constants). It is argued that the method is simple (in particular, no powerdomains are needed), natural (it captures the intuitive operational behavior of a cache), yet more expressive than existing methods (it is the first exact collecting interpretation for either lazy or higher-order programs). Paul Hudak |
POPL | 1 |
| 1988 | An algebraic model for divide-and-conquer and its parallelism
Zhijing G. Mou, Paul Hudak |
J. Supercomput. | 2 |
| 1986 | Memory Coherence in Shared Virtual Memory SystemsabstractThis paper studies the memory coherence problem in designing and implementing a shared virtual memory on looselycoupled multiprocessors.Two classes of algorithms for solving the problem are presented.A prototype shared virtual memory on an Apollo ring has been implemented based on these algorithms.Both theoretical and practical results show that the memory coherence problem can indeed be solved efficiently on a loosely-coupled multiprocessor. Kai Li 0001, Paul Hudak |
PODC | 2 |
| 1986 | Para-Functional Programming: A Paradigm for Programming Multiprocessor SystemsabstractOne of the most important pragmatic advantages of functional languages is that concurrency in a program is implicit -- there is no need for special constructs to express parallelism as is required in most conventional languages. Furthermore, it is fairly easy for compilers to automatically determine the concurrency as a step toward decomposing a program for execution on a suitable parallel architecture. Yet it is often the case that one knows precisely the optimal decomposition for execution on a particular machine, and one can never expect a compiler to determine such optimal mappings in all cases. This paper is concerned with ways to allow the programmer to explicitly express this mapping of program to machine, by using annotations that, given a few minor constraints, cannot alter the functional semantics of the program. We show through several detailed examples the expressiveness and conciseness of the resulting para-functional programming methodology, using an experimental language called ParAlfl based on our ideas. We also give a formal denotational description of the mapping semantics using a notion of execution trees.This research was supported in part by NSF Grants DCR-8403304 and DCR-8451415, and a Faculty Development Award from IBM. Paul Hudak, Lauren Smith |
POPL | 1 |
| 1986 | Higher-Order Strictness Analysis in Untyped Lambda CalculusabstractA function is said to be strict in one of its formal parameters if, in all calls to the function, either the corresponding actual parameter is evaluated, or the call does not terminate. Detecting which arguments a function will surely evaluate is a problem that arises often in program transformation and compiler optimization. We present a strategy that allows one to infer strictness properties of functions expressed in the lambda calculus. Our analysis improves on previous work in that (1) a set-theoretic characterization of strictness is used that permits treatment of free variables, which in turn permits a broader range of interpretations, and (2) the analysis provides an effective treatment of higher-order functions. We also prove a result due to Meyer [15]: the problem of first-order strictness analysis is complete in deterministic exponential time. However, because the size of most functions is small, the complexity seems to be tractable in practice.This research was supported in part by NSF Grant MCS-8302018, and a Faculty Development Award from IBM. Paul Hudak |
POPL | 1 |
| 1986 | A New List Compaction MethodabstractAbstract List compaction, or so‐called ‘cdr‐coding’, can greatly reduce the storage needs of list processing languages. However, existing methods do not perform well when several lists are being constructed simultaneously from the same heap, since the non‐contiguous nature of the cells being allocated eliminates the opportunity for compaction. This situation arises not only in true parallel systems sharing a common memory, and sequential systems supporting multiple processes, but also quite often in purely sequential systems, where it is not uncommon to build several different lists simultaneously within a single loop. In this paper, a new list compaction method is presented that performs well during both sequential and ‘parallel’ list generation. The method is essentially a generalization of cdr‐coding, in which lists are represented explicitly as linked vectors rather than implicitly as compacted memory. In addition, an encoding scheme is used that is as simple or simpler than all known encodings, and destructive operations are supported with no greater overhead than existing schemes. Performance figures in a simulated environment suggest that the strategy consistently performs better than conventional cdr‐coding, with essentially the same complexity. Kai Li 0001, Paul Hudak |
Softw. Pract. Exp. | 2 |
| 1985 | Efficient Distributed Evaluation of Functional Programs Using Serial Combinators
Paul Hudak, Benjamin Goldberg 0001 |
ICPP | 1 |
| 1985 | The Aggregate Update Problem in Functional Programming SystemsabstractWe discuss the problem of efficiently implementing aggregates (contiguous data structures) such as arrays in functional programming systems. Simple changes to an aggregate conceptually involve making a new copy of the aggregate differing only in the changed component, but such copying can be expensive. We present both static and dynamic techniques for avoiding this copying, and argue that they allow one to program functionally using aggregates, without loss of efficiency over conventional programs.1 Paul Hudak, Adrienne G. Bloss |
POPL | 1 |
| 1985 | Distributed Execution of Functional Programs Using Serial CombinatorsabstractA general strategy for automatically decomposing and dynamically distributing a functional program is discussed. The strategy is suitable for parallel execution on multiprocessor architectures with no shared memory. It borrows ideas from data flow and reduction machine research on the one hand, and from conventional compiler technology for sequential machines on the other. One of the more troublesome issues in such a system is choosing the right granularity for the parallel tasks. As a solution, the authors describe a program transformation technique based on serial combinators that offers in some sense just the right granularity for this style of computing, and that can be fine-tuned for particular multiprocessor architectures. Simulation demonstrates the success of this approach. Paul Hudak, Benjamin Goldberg 0001 |
IEEE Trans. Computers | 1 |
| 1984 | A Combinator-Based Compiler for a Functional LanguageabstractArticle Free Access Share on A combinator-based compiler for a functional language Authors: Paul Hudak Yale University, Department of Computer Science Yale University, Department of Computer ScienceView Profile , David Kranz Yale University, Department of Computer Science Yale University, Department of Computer ScienceView Profile Authors Info & Claims POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1984 Pages 122–132https://doi.org/10.1145/800017.800523Online:15 January 1984Publication History 24citation0DownloadsMetricsTotal Citations24Total Downloads0Last 12 Months0Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF Paul Hudak, David A. Kranz |
POPL | 1 |
| 1983 | Distributed Task and Memory ManagementabstractA model of distributed graph reduction is described that has features common to many distributed computing systems: a program (represented as a graph) is partitioned and dynamically distributed among an arbitrary number of processing elements having only local store, and computation takes place as tasks are propagated between vertices in the graph. Specific problems are addressed that are inherent in a computing model of this sort, including garbage collection, detecting deadlock, deleting tasks, and the dynamic prioritization of tasks. By characterizing these problems in terms of graph connectivity, a decentralized graph-marking algorithm is shown to provide an effective solution. This algorithm is unique in that it allows marking a distributed graph whose connectivity is continually changing. Paul Hudak |
PODC | 1 |