POPL 2010 - PDF Preprint Papers

POPL 2010 Annual Symposium on Principles of Programming Languages

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed POPL-2010 Paper

click to vote

POPL
2010
ACM

172views Programming Languages» more POPL 2010»

Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification

1 years 11 months ago

Download www.kb.ecei.tohoku.ac.jp

We introduce higher-order, multi-parameter, tree transducers (HMTTs, for short), which are kinds of higher-order tree transducers that take input trees and output a (possibly infi...

Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno

claim paper

Read More »

Disclaimer and Copyright Notice

Sciweavers respects the rights of all copyright holders and in this regard, authors are only allowed to share a link to their preprint paper on their own website. Every contribution is associated with a desciptive image. It is the sole responsibility of the authors to ensure that their posted image is not copyright infringing. This service is compliant with IEEE copyright.

Id	Views	Title	Status
1	172	Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification	claim
2	128	Modular Verification of Security Protocol Code by Typing	claim
3	115	Efficient parallel programming in Poly/ML and Isabelle/ML	claim
4	114	Verified just-in-time compiler on x86	claim
5	113	Reconfigurable asynchronous logic automata: (RALA)	claim
6	113	Lightweight asynchrony using parasitic threads	claim
7	112	Toward a Verified Relational Database Management System	claim
8	112	Automatically Generating Instruction Selectors Using Declarative Machine Descriptions	claim
9	112	Dynamically Checking Ownership Policies in Concurrent C/C++ Programs	claim
10	110	Static Determination of Quantitative Resource Usage for Higher-Order Programs	claim
11	109	Dependent types and program equivalence	claim
12	109	Integrating Typed and Untyped Code in a Scripting Language	claim
13	106	Low-Level Liquid Types	claim
14	106	Nominal System T	claim
15	106	From Program Verification to Program Synthesis	claim
16	106	Contracts Made Manifest	claim
17	105	Paralocks : Role-Based Information Flow Control and Beyond	claim
18	105	A Relational Modal Logic for Higher-Order Stateful ADTs	claim
19	104	Pure Subtype Systems	claim
20	104	Monads in Action	claim
21	103	Compress-and-conquer for optimal multicore computing	claim
22	102	Threesomes, With and Without Blame	claim
23	101	Generating Compiler Optimizations from Proofs	claim
24	100	Dependent Types from Counterexamples	claim
25	100	Modular Session Types for Distributed Object-Oriented Programming	claim
26	98	Type inference for datalog with complex type hierarchies	claim
27	98	Decision Procedures for Algebraic Data Types with Abstractions	claim
28	97	A Verified Compiler for an Impure Functional Language	claim
29	97	A Theory of Indirection via Approximation	claim
30	96	Ypnos: declarative, parallel structured grid programming	claim
31	95	Programming with angelic nondeterminism	claim
32	95	Semantics and Algorithms for Data-dependent Grammars	claim
33	94	Automatic Numeric Abstractions for Heap-Manipulating Programs	claim
34	92	Sequential Verification of Serializability	claim
35	91	Nested interpolants	claim
36	91	Counterexample-Guided Focus	claim
37	91	Structuring the verification of heap-manipulating programs	claim
38	90	Compositional May-Must Program Analysis: Unleashing the Power of Alternation	claim
39	89	Coarse-Grained Transactions	claim
40	89	Program Analysis via Satisfiability Modulo Path Programs	claim
41	88	On the Verification Problem for Weak Memory Models	claim
42	85	Continuity Analysis of Programs	claim
43	80	Parallelizing constraint programs	claim
44	80	A simple, verified validator for software pipelining	claim
45	73	S-Net for multi-memory multicores	claim
46	72	Abstraction-guided synthesis of synchronization	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers