Witnessing (Co)datatypes
Abstract elided by the publisher.
976 papers · page 17 of 49
Fine-Grained Detection of Privilege Escalation Attacks on Browser Extensions
Abstract elided by the publisher.
A Core Calculus for XQuery 3.0 - Combining Navigational and Pattern Matching Approaches
Abstract elided by the publisher.
Segment Abstraction for Worst-Case Execution Time Analysis
Abstract elided by the publisher.
Static Analysis of Spreadsheet Applications for Type-Unsafe Operations Detection
Abstract elided by the publisher.
IsoLATE: A Type System for Self-recursion
Abstract elided by the publisher.
Refinement Types for Incremental Computational Complexity
Abstract elided by the publisher.
Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages
Abstract elided by the publisher.
Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs
Proving program termination is typically done by finding a well-founded ranking function for the program states. Existing termination provers typically find ranking functions using either linear algebra or templates. As such they are often restricted to finding linear ranking fun…
Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs
This paper shows that it is possible to reason about the safety and termination of programs handling potentially cyclic, singly-linked lists using propositional reasoning even when the safety invariants and termination arguments depend on constraints over the lengths of lists. Fo…
A Verified Compiler for Probability Density Functions
Bhat et al. developed an inductive compiler that computes density functions for probability spaces described by programs in a probabilistic functional language. We implement such a compiler for a modified version of this language within the theorem prover Isabelle and give a form…
Analysis of Asynchronous Programs with Event-Based Synchronization
Abstract elided by the publisher.
Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System
Abstract elided by the publisher.
Inter-procedural Two-Variable Herbrand Equalities
Abstract elided by the publisher.
Probabilistic Programs as Spreadsheet Queries
Abstract elided by the publisher.
Composite Replicated Data Types
Abstract elided by the publisher.
A Semantics for Propositions as Sessions
Abstract elided by the publisher.
A Theory of Name Resolution
Abstract elided by the publisher.
Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs
Abstract elided by the publisher.
CoLoSL: Concurrent Local Subjective Logic
Abstract elided by the publisher.