the proceedings contain 44 papers. the topics discussed include: underspecified harnesses and interleaved bugs;towards a program logic for JavaScript;higher-order functional reactive programming in bounded space;the m...
ISBN:
(纸本)9781450310833
the proceedings contain 44 papers. the topics discussed include: underspecified harnesses and interleaved bugs;towards a program logic for JavaScript;higher-order functional reactive programming in bounded space;the marriage of bisimulations and Kripke logical relations;information effects;a language for automatically enforcing privacy policies;probabilistic relational reasoning for differential privacy;access permission contracts for scripting languages;recursive proofs for inductive tree data-structures;symbolic finite state transducers: algorithms and applications;multiple facets for dynamic information flow;deciding choreography realizability;programminglanguages for programmable networks;a compiler and run-time system for network programminglanguages;an abstract interpretation framework for termination;run your research: on the effectiveness of lightweight mechanization;and verification of parameterized concurrent programs by modular reasoning about data and control.
the proceedings contains 32 papers from the 25thacmsigplan-SIGACT symposium on principles of programminglanguages. Topics discussed include: executable code alias analysis;data flow analysis;intermediate language;m...
详细信息
the proceedings contains 32 papers from the 25thacmsigplan-SIGACT symposium on principles of programminglanguages. Topics discussed include: executable code alias analysis;data flow analysis;intermediate language;monadic states;data structures;assembly language;path profiling;JAVA programing languages;interprocedural class analysis;value flow analysis;local and staged type inferences;mobile codes;parallel beta reduction;and multi-threaded imperative languages.
this proceedings contains 37 papers. Topics discussed include fast and accurate flow-insensitive points to analysis, partitioning dataflow analyses, search and imperative programming, unified computation model for fun...
详细信息
this proceedings contains 37 papers. Topics discussed include fast and accurate flow-insensitive points to analysis, partitioning dataflow analyses, search and imperative programming, unified computation model for functional and logic programming, model checking for programminglanguages using VeriSoft, synchronization transformations, polymorphic Pi-calculus, denotational semantics, operational metatheory for functional languages, relational parametricity and units of measure, high level reading and data structure compilation and a polytypic programming language extension.
the proceedings contain 47 papers. the topics discussed include: full abstraction for nominal Scott domains;copatterns: programming infinite structures by observations;on the linear ranking problem for integer linear-...
ISBN:
(纸本)9781450318327
the proceedings contain 47 papers. the topics discussed include: full abstraction for nominal Scott domains;copatterns: programming infinite structures by observations;on the linear ranking problem for integer linear-constraint loops;automating relatively complete verification of higher-order functional programs;abstraction and invariance for algebraically indexed types;static and dynamic semantics of NoSQL languages;quantitative abstraction refinement;the lambda lambda-bar calculus: a dual calculus for unconstrained strategies;universal properties of impure programminglanguages;the power of parameterization in coinductive proof;deadlock-freedom-by-design: multiparty asynchronous global programming;the type discipline of behavioral separation;views: compositional reasoning for concurrent programs;quantitative relaxation of concurrent data structures;and towards fully automatic placement of security sanitizers and declassifiers.
the proceedings contain 22 papers. the topics discussed include: AnnoDomini: from type theory to year 2000 conversion tool;once upon a polymorphic type;improvement in a lazy context: an operational theory for call-by-...
the proceedings contain 22 papers. the topics discussed include: AnnoDomini: from type theory to year 2000 conversion tool;once upon a polymorphic type;improvement in a lazy context: an operational theory for call-by-need;a compositional account of the java virtual machine;a simple, comprehensive type system for java bytecode subroutines;types for mobile ambients;trust and partial typing in open systems of mobile agents;parametric shape analysis via 3-valued logic;aggregate structure identification and its application to program analysis;and principality and decidable type inference for finite-rank intersection types.
the proceedings contain 37 papers. the topics discussed include: proving non-termination;subcubic algorithms for recursive state machines;back to the future: revisiting precise program verification using SMT solvers;a...
ISBN:
(纸本)9781595936899
the proceedings contain 37 papers. the topics discussed include: proving non-termination;subcubic algorithms for recursive state machines;back to the future: revisiting precise program verification using SMT solvers;automatic inference of stationary fields: a generalization of Java's final fields;demand-driven alias analysis for C;A theory of platform-dependent low-level software;generating precise and concise procedure summaries;lifting abstract interpreters to quantified logical domains;relational inductive shape analysis;a theory of contracts for web services;multiparty asynchronous session types;clowns to the left of me, jokers to the right (pearl): dissecting data structures;foundations for structured programming with GADTs;imperative self-adjusting computation;cryptographically sound implementations for typed information-flow security;and on the computational soundness of cryptographically masked flows.
the proceedings contain 51 papers. the topics discussed include: verified squared: does critical software deserve verified tools?;points-to analysis with efficient strong updates;pick your contexts well: understanding...
ISBN:
(纸本)9781450304900
the proceedings contain 51 papers. the topics discussed include: verified squared: does critical software deserve verified tools?;points-to analysis with efficient strong updates;pick your contexts well: understanding object-sensitivity - the making of a precise and scalable pointer analysis;learning minimal abstractions;static analysis of multi-staged programs via unstaging translation;static analysis of interrupt-driven programs synchronized via the priority ceiling protocol;a parametric segmentation functor for fully automatic and scalable array content analysis;step-indexed kripke models over recursive worlds;a shape analysis for optimizing parallel graph programs;correct blame for contracts: no more scapegoating;generative type abstraction and type-level computation;a separation logic for refining concurrent objects;modular reasoning for deterministic parallelism;and expressive modular fine-grained concurrency specification.
the proceedings contain 41 papers. the topics discussed include: on the verification problem for weak memory models;coarse-grained transactions;sequential verification of serializability;compositional may-must program...
ISBN:
(纸本)9781605584799
the proceedings contain 41 papers. the topics discussed include: on the verification problem for weak memory models;coarse-grained transactions;sequential verification of serializability;compositional may-must program analysis: unleashing the power of alternation;continuity analysis of programs;program analysis via satisfiability modulo path programs;a simple, verified validator for software pipelining;a verified compiler for an impure functional language;verified just-in-time compiler on x86;dependent types from counterexamples;low-level liquid types;type inference for datalog with complex type hierarchies;nominal system T;a theory of indirection via approximation;a relational modal logic for higher-order stateful ADTs;decision procedures for algebraic data types with abstractions;automatic numeric abstractions for heap-manipulating programs;static determination of quantitative resource usage for higher-order programs;and toward a verified relational database management system.
the proceedings contain 13 papers. the topics discussed include: a calculus of delayed reductions;multicompatibility for multiparty-session composition;termination in concurrency, revisited;typed equivalence of labele...
ISBN:
(纸本)9798400708121
the proceedings contain 13 papers. the topics discussed include: a calculus of delayed reductions;multicompatibility for multiparty-session composition;termination in concurrency, revisited;typed equivalence of labeled effect handlers and labeled delimited control operators;type-directed program transformation for constant-time enforcement;comprehending queries over finite maps;intuitionistic metric temporal logic;strongly-typed multi-view stack-based computations;and polymorphic typestate for session types;additive cellular automata graded-monadically.
暂无评论