[pl-seminar] CS838 presentations

[Thomas Reps <reps@xxxxxxxxxxx>]

On Friday, May 9, there will be three 20-minute presentations of 
projects from CS838
given in 5331 CS, starting at 9:50.

========================================================
Alisa Maas & Ara Vartanian:

We introduce the problem of the probablistic modelling of programs. We 
borrow
a methodology from natural language processing of assigning probabilities to
productions in source code parse trees. We begin with a maximum likelihood
model implementing Witten-Bell smoothing for interpolation. We then proceed
to make use of scope information to refine the distributions at terminal 
nodes,
an approach which has an analog in coreference resolution in natural 
language.
We then exploit the special structure of source code in conditioning on a
dependency graph among statements yielded from a program slice.

===============================================================
Divy Vasal: Learning a Regular Language from Queries and Counterexamples

A regular language is a formal language that can be expressed using a
regular expression or as a language accepted by a finite automaton. In
computational learning theory, the problem of induction of regular
languages through supervised learning has been investigated for a
variety of subclasses of regular languages. The techniques for regular
language induction can be used in applications such as finding common
patterns in DNA and RNA sequences, obtaining compact representations of
finite languages, document classification and modeling natural language
acquisition by humans amongst others. Regular languages are also used as
models in syntactic pattern recognition tasks and the learning
techniques developed for them can be extended to other domains as well.

In this presentation, I'll talk about two online algorithms for learning
a finite automaton proposed by D Angluin (called L* learning algorithm)
and Kearns-Vazirani respectively. Both the algorithms make use of an
oracle Teacher to which the Learner asks membership and equivalence
queries about strings in the unknown target language L. In reply to a
membership query, the Teacher can return a "yes" or "no" depending on
whether the query string is accepted by L or not respectively. For an
equivalence query, the Learner presents a conjecture or a hypothesis
language L' it has inferred so far in the form of a DFA and the Teacher
returns a counterexample string in the symmetric difference of L and L'
if there exists any. In case L = L', the algorithm halts reporting that
the learned language L' is equivalent to the target language L. A slight
modification of the learning algorithm wherein the Teacher halts if L'
is a superset of a context-free language L reporting that L' is a
regular set over-approximation of L gives a regular language which
accepts all the strings in a context-free language and probably more.

I'll talk about the running times of these algorithms and show their
actual performance for some test examples including randomly generated
DFAs and manually generated context-free languages. I'll conclude by
discussing the open problem of fully learning a context-free language
and related work in this area.

========================================================
Jason Breck: Verifying Parts of a TVLA-Based Separation Logic 
Semi-Decision Procedure in Coq
After giving a high-level overview of my project, I will introduce some of
the basic ideas of the Coq system. I will walk through an elementary
Coq proof. I will discuss the challenges of programming in a system
where all functions are total and so all computations must terminate. I
may briefly discuss constructive logic, or the Curry-Howard
Correspondence, or relate Coq to such 704 lecture topics as type theory,
structural induction, or typed lambda calculus.

I will briefly introduce TVLA and the separation logic tool that is
currently being used in research by Thakur, Reps, and myself, and then
I’ll discuss the problem of verifying consistency rules and update rules
in that TVLA-based system. I’ll present the overall structure of the
Coq code that I built to verify rules. I may discuss key challenges
that I faced, such as the verification of a procedure that computes the
transitive closure of the “next” relation. Then, I will go through the
outline of the verification of one rule; I will talk about the design 
choices
that I made and the proofs that I have completed.