Zhong Shao, Valery Trifonov, Nikolaos Papaspyrou
A certified binary is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow...
Inferring Protein-Protein Interactions Using Interaction Network Topologies (2008)
Alberto Paccanaro, Valery Trifonov, Haiyuan Yu, Mark Gerstein
[ ∗ these authors contributed equally to this work] Abstract — We describe two novel methods for predicting protein interactions, using only the topology of an observed protein interaction...
Abstract A Type System for Certified Binaries ∗ (2008)
Zhong Shao, Bratin Saha, Valery Trifonov, Nikolaos Papaspyrou
A certified binary is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow...
Abstract A Type System for Certified Binaries ∗ (2008)
Zhong Shao, Bratin Saha, Valery Trifonov, Nikolaos Papaspyrou
A certified binary is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow...
BIOINFORMATICS ORIGINAL PAPER Systems biology (2008)
Haiyuan Yu, Alberto Paccanaro, Valery Trifonov, Mark Gerstein
Vol. 22 no. 7 2006, pages 823–829 doi:10.1093/bioinformatics/btl014 Predicting interactions in protein networks by completing defective cliques
Type Inference for Recursively Constrained Abstract Types and its Application to OOP (2008)
Jonathan Eifrig, Scott Smith, Valery Trifonov
We de ne a powerful type inference mechanism with application to object-oriented programming. The types inferred are recursively constrained types, types that come with a system of constraints. These...
Abstract Supporting Binary Compatibility with Static Compilation £ (2008)
Dachuan Yu, Zhong Shao, Valery Trifonov
There is an ongoing debate in the Java community on whether statically compiled implementations can meet the Java specification on dynamic features such as binary compatibility. Static compilation is...
ABSTRACT Fully Reflexive Intensional Type Analysis ∗ (2008)
Valery Trifonov, Bratin Saha, Zhong Shao
Compilers for polymorphic languages can use runtime type inspection to support advanced implementation techniques such as tagless garbage collection, polymorphic marshalling, and flattened data...
Zhong Shao, Valery Trifonov, Nikolaos Papaspyrou
A certified binary is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow...
Christopher League, Zhong Shao, Valery Trifonov
We present an efficient encoding of core Java constructs in a simple, implementable typed intermediate language. The encoding, after type erasure, has the same operational behavior as a standard...
Jonathan Eifrig, Scott Smith, Valery Trifonov
This paper addresses the problem of designing an object-oriented programming language with an effective type inference mechanism. Recently developed programming languages including Standard ML and...
High-Assurance Common Language Runtime (2007)
Andrew Appel, David Walker, Zhong Shao, Valery Trifonov
API, but in practice this guarantee is only as strong as the implementation of the native libraries, the verifier, and the just-in-time (JIT) compiler. Experience has shown that bugs in the native...
Haiyuan Yu, Philip M. Kim, Emmett Sprecher, Valery Trifonov, Mark Gerstein
It has been a long-standing goal in systems biology to find relations between the topological properties and functional features of protein networks. However, most of the focus in network studies has...
Design principles of molecular networks revealed by global comparisons and composite motifs (2006)
Yu, Haiyuan, Xia, Yu, Trifonov, Valery, Gerstein, Mark
Abstract Background Molecular networks are of current interest, particularly with the publication of many large-scale datasets. Previous analyses have focused on topologic structures of individual...
Predicting interactions in protein networks by completing defective cliques (2006)
Haiyuan Yu, Alberto Paccanaro, Valery Trifonov, Mark Gerstein
defective cliques
Design optimization methods for genomic DNA tiling arrays (2006)
Paul Bertone, Valery Trifonov, Joel S. Rozowsky, Falk Schubert, Olof Emanuelsson, John Karro, ...
A recent development in microarray construction entails the unbiased coverage, or tiling, of non-repetitive genomic DNA for the experimental identification of unannotated transcribed sequences and...
Predicting interactions in protein networks by completing defective cliques (2006)
Yu, Haiyuan, Paccanaro, Alberto, Trifonov, Valery, Gerstein, Mark
Datasets obtained by large-scale, high-throughput methods for detecting protein–protein interactions typically suffer from a relatively high level of noise. We describe a novel method for improving...
Design optimization methods for genomic DNA tiling arrays (2005)
Bertone, Paul, Trifonov, Valery, Rozowsky, Joel S., Schubert, Falk, Emanuelsson, Olof, Karro, John, ...
A recent development in microarray research entails the unbiased coverage, or tiling, of genomic DNA for the large-scale identification of transcribed sequences and regulatory elements. A central...
Precision in practice: A type-preserving Java compiler (2003)
Christopher League, Zhong Shao, Valery Trifonov
Abstract. Popular mobile code architectures (Java and.NET) include verifiers to check for memory safety and other security properties. Since their formats are relatively high level, supporting a wide...
A syntactic approach to foundational proof-carrying code (2002)
Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni
Proof-Carrying Code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing...
V.: Supporting Binary Compatibility with Static Compilation (2002)
Dachuan Yu, Zhong Shao, Valery Trifonov
Rights to individual papers remain with the author or the author's employer. Permission is granted for noncommercial reproduction of the work for educational or research purposes. This copyright...
A syntactic approach to foundational proof-carrying code (2002)
Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni
Abstract. Proof-Carrying Code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific...
A type system for certified binaries (2002)
Zhong Shao, Valery Trifonov, Bratin Saha, Nikolaos Papaspyrou
A certified binary is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow...
A syntactic approach to foundational proof-carrying code (2002)
Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni
Proof-Carrying Code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing...
V.: Supporting Binary Compatibility with Static Compilation (2002)
Dachuan Yu, Zhong Shao, Valery Trifonov
There is an ongoing debate in the Java community on whether statically compiled implementations can meet the Java specification on dynamic features such as binary compatibility. Static compilation is...
Supporting Binary Compatibility with Static Compilation (2002)
Dachuan Yu Zhong, Zhong Shao, Valery Trifonov
There is an ongoing debate in the Java community on whether statically compiled implementations can meet the Java specification on dynamic features such as binary compatibility. Static compilation is...
A syntactic approach to foundational proof-carrying code (2002)
Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni
Abstract. Proof-Carrying Code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific...
A syntactic approach to foundational proof-carrying code (2002)
Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni
Proof-Carrying Code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing...
Functional Java bytecode (2001)
Christopher League, Valery Trifonov, Zhong Shao
We describe the design and implementation of λJVM, a functional representation of Java bytecode that makes data flow explicit, verification simple, and that is well-suited for translation into...
Parallel Functional Reactive Programming (2000)
John Peterson, Valery Trifonov, Andrei Serjantov
Abstract. In this paper, we demonstrate how Functional Reactive Programming (FRP), a framework for the description of interactive systems, can be extended to encompass parallel systems. FRP is based...
Parallel Functional Reactive Programming (2000)
John Peterson, Valery Trifonov, Andrei Serjantov
Abstract In this paper, we demonstrate how Functional Reactive Programming (FRP), a framework for the description of interactive systems, can be extended to encompass parallel systems. FRP is based...
Fully reflexive intensional type analysis (2000)
Valery Trifonov, Bratin Saha, Zhong Shao
Compilers for polymorphic languages can use runtime type inspection to support advanced implementation techniques such as tagless garbage collection, polymorphic marshalling, and flattened data...
Parallel Functional Reactive Programming (2000)
John Peterson Valery, John Peterson, Valery Trifonov, Andrei Serjantov
In this paper, we demonstrate how Functional Reactive Programming (FRP), a framework for the description of interactive systems, can be extended to encompass parallel systems. FRP is based on...
Parallel Functional Reactive Programming (2000)
John Peterson, Valery Trifonov, Andrei Serjantov
Abstract In this paper, we demonstrate how Functional Reactive Programming (FRP), a framework for the description of interactive systems, can be extended to encompass parallel systems. FRP is based...
Fully reflexive intensional type analysis (2000)
Bratin Saha, Valery Trifonov, Computer Science
Abstract Compilers for polymorphic languages can use runtime type in-spection to support advanced implementation techniques such as tagless garbage collection, polymorphic marshalling, and...
Intensional analysis of quantified types (2000)
Bratin Saha, Valery Trifonov, Zhong Shao
Compilers for polymorphic languages can use run-time type inspection to support advanced implementation techniques such as tagless garbage collection, polymorphic marshalling, and flattened data...
Safe and principled language interoperation (1999)
Abstract. Safety of interoperation of program fragments written in different safe languages may fail when the languages have different systems of computational effects: an exception raised by an ML...
Representing Java Classes in a Typed Intermediate Language (1999)
Christopher League, Zhong Shao, Valery Trifonov
We propose a conservative extension of the polymorphic lambda calculus (F ! ) as an intermediate language for compiling languages with name-based class and interface hierarchies. Our extension...
Safe and principled language interoperation (1999)
Abstract. Safety of interoperation of program fragments written in different safe languages may fail when the languages have different systems of computational effects: an exception raised by an ML...
Scaling Proof-Carrying Code to Production Compilers and Security Policies (1998)
Appel, Andrew W., Felton, Edward W., Walker, David P., Shao, Zhong, Trifonov, Valery
We have developed high-assurance software protection mechanisms that can be used in component-software platforms (virtual machines such as Sun's Java or Microsoft's .Net). The idea is to leverage...
Type-Preserving Compilation of Featherweight Java (1998)
League, Christopher, Trifonov, Valery, Shao, Zhong
We present an efficient encoding of core Java constructs in a simple, implementable typed intermediate language. The encoding, after type erasure, has the same operational behavior as a standard...
Precision in Practice: A Type-Preserving Java Compiler (1998)
League, Christopher, Shao, Zhong, Trifonov, Valery
Popular mobile code architectures (Java and .NET) include verifiers to check for memory safety and other security properties. Since their formats are relatively high level, supporting a wide range of...
Fully Reflexive Intensional Type Analysis in Type Erasure Semantics (1998)
Saha, Bratin, Trifonov, Valery, Shao, Zhong
Compilers for polymorphic languages must support runtime type analysis over arbitrary source language types for coding applications like garbage collection, dynamic linking, pickling, etc. On the...
Type-Directed Continuation Allocation (1998)
Suppose we translate two different source languages, L(sub1) and L(sub2), into the same intermediate language; can they safely interoperate in the same address space and under the same runtime...
Supporting Binary Compatibility with Static Compilation (1998)
Yu, Dachuan, Shao, Zhong, Trifonov, Valery
There is an ongoing debate in the Java community on whether statically compiled implementations can meet the Java specification on dynamic features such as binary compatibility. Static compilation is...
Type-Preserving Compilation of Featherweight Java (1998)
League, Christopher, Shao, Zhong, Trifonov, Valery
We present an efficient encoding of core Java constructs in a simple, implementable typed intermediate language. The encoding, after type erasure, has the same operational behavior as a standard...
Fully Reflexive Intensional Type Analysis (1998)
Saha, Bratin, Trifonov, Valery, Shao, Zhong
Compilers for polymorphic languages can use runtime type inspection to support advanced implementation techniques such as tagless garbage collection, polymorphic marshalling, and flattened data...
A Type System for Certified Binaries (1998)
Shao, Zhong, Trifonov, Valery, Saha, Bratin, Papaspyrou, Nikolaos
A certified binary is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow...
Intensional Analysis of Quantified Types (1998)
Saha, Bratin, Trifonov, Valery, Shao, Zhong
Compilers for polymorphic languages can use run-time type inspection to support advanced implementation techniques such as tagless garbage collection, polymorphic marshalling, and flattened data...
Representing Java Classes in a Typed Intermediate Language (1998)
League, Christopher, Shao, Zhong, Trifonov, Valery
We propose a conservative extension of the polymorphic lambda calculus F(omega) as an intermediate language for compiling languages with name-based class and interface hierarchies. Our extension...
A Syntactic Approach to Foundational Proof-Carrying Code (1998)
Hamid, Nadeem A., Shao, Zhong, Trifonov, Valery, Monnier, Stefan, Ni, Zhaozhong
Proof-Carrying Code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing...
Type-directed continuation allocation (1998)
Abstract. Suppose we translate two different source languages, £¥ ¤ and £§ ¦ , into the same intermediate language; can they safely interoperate in the same address space and under the same...
Type-Directed Continuation Allocation (1998)
. Suppose we translate two different source languages, L1 and L2 , into the same intermediate language; can they safely interoperate in the same address space and under the same runtime system? If L1...
Type-directed continuation allocation (1998)
Abstract. Suppose we translate two different source languages, £¥ ¤ and £§ ¦ , into the same intermediate language; can they safely interoperate in the same address space and under the same...
Properties and applications of polymorphic constrained types--[microform] /--Valery Trifonov. (1997)
Vita.
Subtyping constrained types. Revised Draft (1996)
A constrained type is a type that comes with a set of subtyping constraints on variables occurring in the type. Constrained type inference systems are a natural generalization of Hindley/Milner type...
Subtyping Constrained Types (1996)
Constrained type systems are a natural generalization of Hindley/Milner type inference to languages with subtyping. This paper develops several subtyping relations on constrained types. We establish...
Subtyping constrained types (1996)
Abstract. A constrained type is a type that comes with a set of subtyping constraints on variables occurring in the type. Constrained type inference systems are a natural generalization of...
Sound polymorphic type inference for objects (1995)
Jonathan Eifrig, Scott Smith, Valery Trifonov
A polymorphic, constraint-based type inference algorithm for an object-oriented language is defined. A generalized form of type, polymorphic recursively constrained types, are inferred. These types...
Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, Jonathan Eifrig, Scott F. Smith, Valery Trifonov, ...
Giving types to binary methods causes significant problems for object-oriented language designers and programmers. This paper offers a comprehensive description of the problems arising from typing...
Application of OOP type theory: State, decidability, integration (1994)
Jonathan Eifrig, Scott Smith, Valery Trifonov, Amy Zwarico
Important strides toward developing expressive yet semantically sound type systems for object-oriented programming languages have recently been made by Cook, Bruce, Mitchell, and others. This paper...
A simple interpretation of OOP in a language with state (1993)
Jonathan Eifrig, Scott Smith, Valery Trifonov, Amy Zwarico
Giving a complete semantics to strongly typed object-oriented programming is a well-known research problem. Recent work has made significant strides toward solving this problem. However, in most of...
Design optimization methods for genomic DNA tiling arrays
Bertone, Paul, Trifonov, Valery, Rozowsky, Joel S., Schubert, Falk, Emanuelsson, Olof, Karro, John, ...
A recent development in microarray research entails the unbiased coverage, or tiling, of genomic DNA for the large-scale identification of transcribed sequences and regulatory elements. A central...
Design optimization methods for genomic DNA tiling arrays
Bertone, Paul, Trifonov, Valery, Rozowsky, Joel S., Schubert, Falk, Emanuelsson, Olof, Karro, John, ...
A recent development in microarray research entails the unbiased coverage, or tiling, of genomic DNA for the large-scale identification of transcribed sequences and regulatory elements. A central...
Design principles of molecular networks revealed by global comparisons and composite motifs
Yu, Haiyuan, Xia, Yu, Trifonov, Valery, Gerstein, Mark
A global comparison of the four basic molecular networks in yeast - regulatory, co-expression, interaction and metabolic - reveals general design principles.
Yu, Haiyuan, Kim, Philip M, Sprecher, Emmett, Trifonov, Valery, Gerstein, Mark
It has been a long-standing goal in systems biology to find relations between the topological properties and functional features of protein networks. However, most of the focus in network studies has...