Author name cluster

Ramesh Viswanathan

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

I&C Journal 2014 Journal Article

Least upper bounds for probability measures and their applications to abstractions

Rohit Chadha
Mahesh Viswanathan
Ramesh Viswanathan

Least upper bounds play an important role in defining the semantics of programming languages, and in abstract interpretations. In this paper, we identify conditions on countable ordered measurable spaces that ensure the existence of least upper bounds for all sets of probability measures. These conditions are shown to be necessary as well — for any measurable space not satisfying these conditions, there are (finite) sets of probability measures for which no least upper bound exists. For measurable spaces meeting these conditions, the existence of least upper bounds is established constructively. Based on this least upper bound construction, we present a novel abstraction method applicable to Discrete Time Markov Chains (DTMCs), Markov Decision Processes (MDPs), and Continuous Time Markov Chains (CTMCs). The main advantage of the new abstraction techniques is that the resulting abstract models are purely probabilistic that may be more amenable to automated analysis than models with both nondeterministic and probabilistic transitions which arise from previously known abstraction techniques.

Details DOI

I&C Journal 1996 Journal Article

Standard ML–NJ Weak Polymorphism and Imperative Constructs

John Mitchell
Ramesh Viswanathan

Standard ML of New Jersey (SML–NJ) uses “weak type variables” to restrict the polymorphic use of functions that may allocate reference cells, manipulate continuations, or use exceptions. However, the type system used in the SML–NJ compiler has not previously been presented in a form other than source code nor proved correct. We present a set of typing rules, based on analysis of the concepts underlying “weak polymorphism”, that appears to subsume the implemented algorithm and uses type variables of only a slightly more general nature than the compiler. One insight in the analysis is that allowing a variable to occur both “ordinarily” and “weakly” in a type permits a simpler and more flexible formulation of the typing rules. In particular, we are able to treat applications of polymorphic functions to imperative arguments with greater flexibility than SML–NJ. The soundness of the type system is proved for imperative code using operational semantics, by showing that evaluation preserves typability. By incorporating assumptions about memory addresses in the type system, we avoid proofs by co-induction.

Details DOI