Christopher Johnson has nearly two decades of experience as a successful job recruiter for technical and professional positions in Vermont. He is the Founder and Director of Technical Connection, Inc. (http://www.vttechjobs.com/), which provides full-time technical and professional job placement services, and offers technical contract employment, assigned to top companies in Vermont.

Chris Johnson will discuss current hiring trends in hi-tech Vermont companies and share his insights into the market-place of jobs in technology.

Join us as Professor Damon discusses his experiences over the course of fifteen years in industry, and the founding two object database companies.

Current software attacks often build on exploits that subvert machine-code execution. The enforcement of a basic safety property, Control-Flow Integrity (CFI), can prevent such attacks from arbitrarily controlling program behavior.

CFI enforcement is simple, and its guarantees can be established formally, even with respect to powerful adversaries. Moreover, CFI enforcement is practical: it is compatible with existing software and can be efficiently implemented. Finally, CFI guarantees are a useful foundation for analysis, processing, and the establishment of further properties of the software.

CFI derives its security benefits from constraining low-level operations to conform more closely to the high-level programming language semantics. CFI generalizes, or can subsume, popular mechanisms for reducing this discrepancy between the hardware and software semantics.

The logical framework Twelf provides an experimental platform to specify, implement and execute formal systems. One of its applications is in proof-carrying code and proof-carrying authentication, where it is successfully used to specify and verify formal guarantees about the run-time behavior of programs. These real-world applications have exposed some critical bottlenecks: execution of many logical specifications is severely hampered and some are not executable at all, thereby limiting its application in practice.

In this talk, I will describe three optimizations which substantially improve the performance and extend the power of the existing system. First, I give an optimized unification algorithm for logical frameworks which allows us to eliminate unnecessary occurs-checks. Second I present a novel execution model based on selective memoization and third I will discuss term indexing techniques to sustain performance in large-scale examples. As experimental results will demonstrate, these optimizations taken together constitute a significant step toward exploring the full potential of logical frameworks in real-world applications.

Richard Stallman, founder of the Free Software Foundation, will speak about the purpose, goals, philosophy, methods, status, and future prospects of the GNU operating system, which in combination with the kernel Linux is now used by an estimated 17 to 20 million users world wide.

A static algorithm is one that computes the result of a query about the output for a single, fixed input. For example, a static sorting algorithm is one that takes as input a set of keys, and permits queries about the relative order of these keys according to some ordering relation. A dynamic, or incremental, algorithm is one that permits queries about the output to be interleaved with operations that incrementally modify the input. For example, a dynamic sorting algorithm is one that would permit insertion or deletion of keys to be interleaved with queries about their relative ordering. Self-adjusting computation is a method for deriving a dynamic algorithm from a static algorithm by applying three main techniques: adaptivity, which permits the output of an algorithm to be adjusted to reflect changes to its input; selective memoization, which permits re-use of results based on accurate control flow information rather than simple call patterns; and adaptive memoization, which permits re-use of incorrect computations by adaptation. These techniques are realized as linguistic mechanisms in a statically typed functional language whose type system guarantees that the effects of an input modification are correctly propagated to their outputs, thereby ensuring that the dynamic algorithm is correct relative to its static counterpart. Using these methods we obtain dynamic versions of several well-known algorithms, including a dynamic version of Quicksort that adapts to insertions and deletions in expected logarithmic time. (Joint work with Umut A. Acar and Guy E. Blelloch)

There is a wide range of sensor networks, ranging from small, power-constrained embedded sensing networks (used, e.g., for monitoring structural response or contaminant transport in the environment) to large, high-bandwidth, powered remote sensing networks (e.g., meteorological radar networks, and video sensing networks). Despite their obvious differences, these sensor networks also have many similarities and share a number of common technical challenges. In this talk, we consider the class of large, high-bandwidth, powered remote sensing networks, and identify networking, storage, and computing research challenges posed by such systems. We also consider the similarities and differences between these systems and their small, power-constrained embedded sensing counterparts. We illustrate these issues drawing on our experiences in designing and implementing a dense network of meteorological radars whose goals is to collaboratively and adaptively sense the lowest few kilometers of the earth's atmosphere. This testbed system is one the efforts being undertaken in the Center for Collaborative Adaptive Sensing of the Atmosphere, a recently award NSF Engineering Research Center led by the University of Massachusetts.

Server-side Web applications have grown increasingly common, sometimes even replacing brick and mortar as the principal interface of corporations. Correspondingly, Web browsers grow ever more powerful, empowering users to attach bookmarks, switch between pages, clone windows, and so forth. As a result, Web interactions are not straight-line dialogs but complex nets of interaction steps.

In practice, programmers are unaware of or are unable to handle these nets of interaction, making the Web interfaces of even major organizations buggy and thus unreliable. These problems are likely to grow worse when the output of Web services are processed by programs rather than humans. Even when programmers do address these constraints, the resulting programs have a seemingly mangled structure, making them difficult to develop and hard to maintain.

In this talk, I will describe these interactions and then show how programming language ideas can shed light on the resulting problems and present solutions at various levels.

Mathematics, including formal logic and theoretical Computer Science, is comprised of theorems that are often regarded and presented as Law, unchanging and true. However, human mathematical knowledge and technique has evolved over time, concurrently with perspectives on the nature of mathematical facts-- that is, with philosophies of mathematics. Furthermore, successful technical developments have directly affected philosophy, just as shifts in philosophy have instigated technical developments. Paradoxes, which indicate apparent contradictions of fact in reasoning systems, have historically challenged the technical and philosophical status quo in mathematics, spurring advances and highlighting the tension between theory and practice. Thus, paradoxes are prime case studies for considering the ontological status of mathematics, and for understanding the history of mathematics. In this talk, several paradoxes in the history of mathematics and logic will be reviewed, and discussed in light of their effect on technique and/or philosophy. In particular, we will discuss one (the Kleene-Rosser paradox) that has profound significance for the mathematical theory underlying modern Computer Science.

Richard Stallman, founder of the Free Software Foundation, will explain how software patents obstruct software development. Software patents are patents that cover software ideas. They restrict the development of software, so that every design decision brings a risk of getting sued. Patents in other fields restrict factories, but software patents restrict every computer user. Economic research shows that they even retard progress.

As a natural language semanticist, I strive to scientifically explain why "every student passed" entails "every diligent student passed", why "a man is mugged every 11 seconds" is ambiguous, and why "nobody asked any question" sounds better than "everybody asked any question". Making a linguistic theory is like specifying a programming language: one typically devises a type system to characterize what utterances are acceptable, then a denotational semantics to explain which statements entail which other ones. Via this connection, programming and natural language research can inform each other; in particular, computational side effects are intimately related to referential opacity in natural languages. In this talk, I will illustrate this link by using continuations and composable contexts, concepts from the study of side effects in programming languages, to analyze quantification, a natural language phenomenon. My examples will be drawn from English (and Mandarin Chinese, if time permits). No prior knowledge of linguistics will be assumed.

(This talk describes joint work with Chris Barker and Stuart Shieber.)