13 citations · 18 across the 6 of their papers we have counts for
6 papers
DCDChain: A Credible Architecture of Digital Copyright Detection Based on Blockchain
Zhili Chen, Yuting Wang, Tianjiao Ni
Copyright detection is an effective method to prevent piracy. However, untrustworthy detection parties may lead to falsified detection results. Due to its credibility and tamper re…
Schematic Polymorphism in the Abella Proof Assistant
Gopalan Nadathur, Yuting Wang
The Abella interactive theorem prover has proven to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the…
A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs
Yuting Wang
We argue that the implementation and verification of compilers for functional programming languages are greatly simplified by employing a higher-order representation of syntax know…
A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
Yuting Wang, Gopalan Nadathur
We describe an approach to the verified implementation of transformations on functional programs that exploits the higher-order representation of syntax. In this approach, transfor…
Towards Extracting Explicit Proofs from Totality Checking in Twelf
Yuting Wang, Gopalan Nadathur
The Edinburgh Logical Framework (LF) is a dependently type lambda calculus that can be used to encode formal systems. The versatility of LF allows specifications to be constructed…
Reasoning About Higher-Order Relational Specifications
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek +1
The logic of hereditary Harrop formulas (HH) has proven useful for specifying a wide range of formal systems. This logic includes a form of hypothetical judgment that leads to dyna…