yusuke1997/dblp-id-title huggingface dataset:
Polymorphic Type Inference and Assignment
A Methodology for Lisp Program Construction from Examples
Automatic Decomposition of Scientific Programs for Parallel Execution
Automatically comparing memory consistency models
Monadic second-order logic on finite sequences
Final Data Tye Specifications: A New Data Type Specification Method
A constraint-based approach to solving games on infinite graphs
Analyzing security protocols with secrecy types and logic programs
Temporal Proof Methodologies for Real-time Systems
Representing Layered Monads
Inferring Types in Smalltalk
An Interpretation of Objects and Object Types
Compilation of Data-Driven Programs for Synchronous Execution
A generic approach to the static analysis of concurrent programs with procedures
The design and implementation of typed scheme
The next 700 data description languages
Shape Types
On the analysis of interacting pushdown systems
Dynamic heap type inference for program understanding and debugging
A Flexible Approach to Interprocedural Data Flow Analysis and Programs with Recursive Data Structures
Parameter-Passing and the Lambda Calculus
Axiomatic Definitions of Programming Languages: A Theoretical Assessment
Copatterns: programming infinite structures by observations
Derivation of Efficient DAG Marking Algorithms
Symbolic transfer function-based approaches to certified compilation
Typed Memory Management in a Calculus of Capabilities
Component-based synthesis for complex APIs
Ownership types for object encapsulation
Dynamic Typing in a Statically-Typed Language
Logic and Inheritance
From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification
A Semantic Model for Parallel Systems with Scheduling
A posteriori environment analysis with Pushdown Delta CFA
Context logic as modal logic: completeness and parametric inexpressivity
Compiler Optimizations for Asynchronous Systolic Array Programs
Parsing expression grammars: a recognition-based syntactic foundation
Towards Programming with Knowledge Expressions
Realistic Compilation by Program Transformation
Automatic granularity-aware parallelization of programs with predicates, functions, and constraints: invited talk
A Straightforward Denotational Semantics for Non-Determinant Data Flow Programs
Static analysis of multi-staged programs via unstaging translation
Formal certification of a compiler back-end or: programming a compiler with a proof assistant
Type Isomorphisms in a Type-Assignment Framework
Automatic inference of stationary fields: a generalization of java's final fields
Focusing on pattern matching
Extracting F(omega)'s Programs from Proofs in the Calculus of Constructions
Relating Total and Partial Correctness Interpretations of Non-Deterministic Programs
Automatic Verification of Parameterized Linear Networks of Processes
LMS-Verify: abstraction without regret for verified systems programming
New Control Structures to Aid Gotolessness
Program Optimization and Exception Handling
Symbolic finite state transducers: algorithms and applications
On the Advantages of Free Choice: A Symmetric and Fully Distributed Solution to the Dining Philosophers Problem
A Categorized Bibliography on Incremental Computation
Manifest Types, Modules, and Separate Compilation
Resource usage analysis
Types are Not Sets
Systems Programming in Concurrent Prolog
Nested interpolants
Sound Modular Verification of C Code Executing in an Unverified Context
A query language for data parallel programming: invited talk
Efficient Flow-Sensitive Interprocedural Computation of Pointer-Induced Aliases and Side Effects
Checking That Finite State Concurrent Programs Satisfy Their Linear Specification
A combination framework for tracking partition sizes
A Model and Temporal Proof System for Networks of Processes
Plan B: a buffered memory model for Java
Iterated Register Coalescing
Parametric Shape Analysis via 3-Valued Logic
Programming the world of uncertain things (keynote)
Abstract satisfaction
CakeML: a verified implementation of ML
Lazy evaluation and delimited control
Semantics-Directed Machine Architecture
Bidirectionalization for free! (Pearl)
Induction Variables in Very High Level Languages
A Maximum-Flow Approach to Anomaly Isolation in Unification-Based Incremental Type Inference
Efficient algorithms for isomorphisms of simple types
Is the Interesting Part of Process Logic Uninteresting - A Translation from PL to PDL
A complete, co-inductive syntactic theory of sequential control and state
Comparing the performance of concurrent linked-list implementations in Haskell
Decision procedures for algebraic data types with abstractions
Databases and Programming: Two Subjects Divided by a Common Language?
You and your graduate research
The Concurrent Logic Programming Language CP: Definition and Operational Semantics
On the Relations Computable by a Class of Concurrent Automata
On the computational soundness of cryptographically masked flows
Opening remarks
Verification of parameterized concurrent programs by modular reasoning about data and control
Proceedings of the POPL 2009 Workshop on Declarative Aspects of Multicore Programming, DAMP 2009, Savannah, GA, USA, January 20, 2009
A Language with Distributed Scope
Minimization of symbolic automata
The first-order theory of subtyping constraints
Generalized Fair Termination
Separation and information hiding
A foundation for flow-based program matching: using temporal logic and model checking
Quasi-Linear Types
A Dynamic Extent Control Operator for Partial Continuations
Full Abstraction for Signal Flow Graphs
First-Class Macros have Types
Speculative N-Way barriers
Principal Type Schemes for Gradual Programs
Recognizing Substrings of LR(k) Languages in Linear Time
Principal Type-Schemes for Functional Programs
Type-Directed Partial Evaluation
Improvement in a Lazy Context: An Operational Theory for Call-by-Need
Automatic Binding Time Analysis for a Typed Lambda-Calculus
Library abstraction for C/C++ concurrency
Program Logic Without Binding is Decidable
Positive Subtyping
Linear Continuations
Interruptible iterators
The space cost of lazy reference counting
The Equivalence Problem for Program Schemata with Nonintersecting Loops
Proving that programs eventually do something good
Pure subtype systems
Towards Fully Abstract Semantics for Local Variables
Higher-Order Strictness Analysis in Untyped Lambda Calculus
Concurrent Haskell
A type system for borrowing permissions
Composing Processes
Contextual effects for version-consistent dynamic software updatingalland safe concurrent programming
Combining Generational and Conservative Garbage Collection: Framework and Implementations
A separation logic for refining concurrent objects
The ins and outs of gradual type inference
The essence of compiling with traces
Programming Languages, Natural Languages, and Mathematics
Code Generation for Machines with Multiregister Operations
Sound predictive race detection in polynomial time
An Operational Framework for Value-Passing Processes
A proof system for separation logic with magic wand
A Logical View of Composition and Refinement
Deriving Algorithms From Type Inference Systems: Application to Strictness Analysis
Coinductive techniques, from automata to coalgebra
Formal verification of translation validators: a case study on instruction scheduling optimizations
Taming release-acquire consistency
Fast Interprocedural Alias Analysis
Checking NFA equivalence with bisimulations up to congruence
Trace-Based Program Analysis
On the Composition of Processes
Unifying type checking and property checking for low-level code
Combining subsumption and binary methods: an object calculus with views
Resource Bound Certification
Abstract acceleration of general linear loops
The Smalltalk-76 Programming System
Applicative Programming and Digital Design
Structured Exception Handling
Unification in Many-Sorted Algebras as a Device for Incremental Semantic Analysis
Dynamically checking ownership policies in concurrent c/c++ programs
A logical account of pspace
Constraints as control
A type-directed abstraction refinement approach to higher-order model checking
A Formal Model of Procedure Calling Conventions
Small Domains Spell Fast Strictness Analysis
Semantics of transactional memory and automatic mutual exclusion
Contracts made manifest
Modular, higher-order cardinality analysis in theory and practice
A Simplifier Based on Efficient Decision Algorithms
Polymorphic typed defunctionalization
A Mathematical Approach to Language Design
An Improvement to Bottom-up Tree Pattern Matching
Procedure Referencing Environments in SL5
Learning invariants using decision trees and implication counterexamples
Genesis: synthesizing forwarding tables in multi-tenant networks
Corrigendum: Decidable Bounded Quantification
Fast polyhedra abstract domain
Points-to Analysis in Almost Linear Time
A hierarchical model of data locality
A Demand-Driven Set-Based Analysis
Synthesis of interface specifications for Java classes
From Boolean to quantitative notions of correctness
Type-Safe Linking and Modular Assembly Language
Associated types with class
A type system for certified binaries
Lustre: A Declarative Language for Programming Synchronous Systems
Threesomes, with and without blame
Abstraction Mechanisms in the Beta Programming Language
Binding Time Optimization in Programming Languages: Some Thoughts Toward the Design of an Ideal Language
Partial Evaluation of High-Level Imperative Programming Languages, with Applications in Hard Real-Time Systems
Automating relatively complete verification of higher-order functional programs
Associating synchronization constraints with data in an object-oriented language
Deciding Type Equivalence with Singleton Kinds
Dependent types and multi-monadic effects in F
Theoretical foundations for compensations in flow composition languages
Decisions for "Type" in APL
Principal typings for Java-like languages
Generating compiler optimizations from proofs
(Optimal) Duplication is not Elementary Recursive
Expressing Interesting Properties of Programs in Propositional Temporal Logic
Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executables
Efficient Algorithms for Structural Similarity of Grammars
A Combinator-Based Compiler for a Functional Language
Adaptive functional programming
Conjugate Hylomorphisms - Or: The Mother of All Structured Recursion Schemes
Masked types for sound object initialization
Types as Intervals
Operational semantics for multi-language programs
Engineering formal metatheory
Reasoning About Programs
On the relationship between higher-order recursion schemes and higher-order fixpoint logic
Run your research: on the effectiveness of lightweight mechanization
Compiling Strictness into Streams
Guarded recursive datatype constructors
Maximal Static Expansion
Practical affine types
A Meta-Language and System for Nonlocal Incremental Attribute Evaluation in Language-Based Editors
Low-pain, high-gain multicore programming in Haskell: coordinating irregular symbolic computations on multicore architectures
Secure implementations of typed channel abstractions
Concurrent programming constructs in multi-engine prolog: parallelism just for the cores (and not more!)
Generative type abstraction and type-level computation
An Algebraic Model for String Patterns
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
Synchronization Transformations for Parallel Computing
Transitions in Extendible Arrays
Grids: A New Program Structuring Mechanism Based on Layered Graphs
TDVMP: Improved Virtual Machine-Based Software Protection with Time Diversity
Semantic Foundations of Concurrent Constraint Programming
Semantics and algorithms for data-dependent grammars
Sparse Code Motion
A Dynamic Logic of Multiprocessing with Incomplete Information
Coming to terms with quantified reasoning
A Logic for Partially Specified Data Structures
Call by Name, Assignment, and the Lambda Calculus
Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
A Rewriting Semantics for Program Dependence Graphs
Access permission contracts for scripting languages
A variant of the Chaum voter-verifiable scheme
Static Analysis to Reduce Synchronization Costs in Data-Parallel Programs
Automatic Design of Data Processing Systems
Direct Implementation of Compiler Specifications or the Pascal P-code Compiler Revisited
From MinX to MinC: semantics-driven decompilation of recursive datatypes
Is it a Tree, a DAG, or a Cyclic Graph? A Shape Analysis for Heap-Directed Pointers in C
Formal Parametric Polymorphism
A Types-as-Sets Semantics for Milner-Style Polymorphism
Process Logic
Channel dependent types for higher-order mobile processes
Typechecking Records and Variants in a Natural Extension of ML
Relational Parametricity and Local Variables
Incremental Polymorphic Type Checking in B
Principles of OBJ2
Practical Error Recovery in LR Parsing
Specification Inference Using Context-Free Language Reachability
The Complexity of Type Inference for Higher-Order Typed Lambda Calculi
Loop transformations: convexity, pruning and optimization
Semantic Parallelization: A Practical Exercise in Abstract Interpretation
Prime Subprogram Parsing of a Program
Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 1983
An Introduction to Logical Relations and Parametric Polymorphism - Tutorial
Sigma*: symbolic learning of input-output specifications
Almost Control-Free (Indeterministic) Parallel Computation on Permit Schemes
A Constructive Logic of Multiple Subtyping
Cache and I/O efficent functional algorithms
Efficient parallel programming in Poly/ML and Isabelle/ML
Systematic Design of Program Analysis Frameworks
Inductive Methods for Reasoning about Abstract Data Types
Remote Attribute Updating for Language-Based Editors
Incremental Data Flow Analysis via Dominator and Attribute Updates
Computer Assisted Application Definition
Anytime, Anywhere: Modal Logics for Mobile Ambients
Programming with angelic nondeterminism
Abstract non-interference: parameterizing non-interference by abstract interpretation
N -synchronous Kahn networks: a relaxed model of synchrony for real-time systems
Model Checking and Abstraction
Automatic Improvement of Programs in Very High Level Languages
The third homomorphism theorem on trees: downward & upward lead to divide-and-conquer
A Type System for Prototyping Languages
Symbolic computation of differential equivalences
Abstraction and invariance for algebraically indexed types
Communication with Directed Logic Variables
Programming Primitives for Database Languages
Structuring the verification of heap-manipulating programs
Proceedings of the POPL 2012 Workshop on Declarative Aspects of Multicore Programming, DAMP 2012, Philadelphia, PA, USA, Saturday, January 28, 2012
The SLAM project: debugging system software via static analysis
A semantics-based approach to malware detection
Abstract Types Have Existential Type
Abstractions from proofs
Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994
Applying quantitative semantics to higher-order quantum computing
Generalized Left Corner Parsing
On interference abstractions
The story of Arjun Guha, or: the arc of a research project
Verifying Infinite State Processes with Sequential and Parallel Composition
Formal Analysis of CRT-RSA Vigilant's Countermeasure Against the BellCoRe Attack: A Pledge for Formal Methods in the Field of Implementation Security
Interactive Proof Checking
Principal type inference for GADTs
Compress-and-conquer for optimal multicore computing
Compilation and Delayed Evaluation in APL
Algebraic Effects, Linearity, and Quantum Programming Languages
Oracle-based checking of untrusted software
Program verification as probabilistic inference
Reduction: A New Method of Proving Properties of Systems of Processes
A Natural Semantics for Lazy Evaluation
Interprocedural analysis of asynchronous programs
Isomorphisms of generic recursive polynomial types
Optimizing synthesis with metasketches
Semantics for Communication Primitives in an Polymorphic Language
The next mainstream programming language: a game developer's perspective
Positive supercompilation for a higher order call-by-value language
Policy framings for access control
Functional Computation as Concurrent Computation
A Typed Language for Distributed Mobile Processes (Extended Abstract)
Scrap your boilerplate with XPath-like combinators
Automated Synthesis of Interface Adapters for Reusable Classes
A Linear Time Algorithm for Placing phi-nodes
The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013
Using Parameterized Signatures to Express Modular Structure
Stochastic invariants for probabilistic termination
A Semantic Model of Types and Machine Instructions for Proof-Carrying Code
The Reflexive CHAM and the Join-Calculus
Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989
Using static analysis to validate the SAML single sign-on protocol
Stream fusion, to completeness
Annotations for Distributed Programming in Logic
Extracting queries by static analysis of transparent persistence
PADS/ML: a functional data description language
A Compositional Approach to Superimposition
A verifiable SSA program representation for aggressive compiler optimization
A rely-guarantee-based simulation for verifying concurrent program transformations
Dijkstra monads for free
A semantics for procedure local heaps and its abstractions
System f-omega with equirecursive types for datatype-generic programming
Automatic Discovery of Linear Restraints Among Variables of a Program
A relational modal logic for higher-order stateful ADTs
Stochastic Processes as Concurrent Constraint Programs
Modes, Values, and Expressions
Geometry of synthesis III: resource management through type inference
Expressiveness of the Operation Set of a Data Abstraction
Making prophecies with decision predicates
Coordinating First-Order Multiparty Interactions
Strictness Analysis and Denotational Abstract Interpretation
Program Improvement by Source to Source Transformation
Symmetric lenses
A Lazy Evaluator
Static Typing for Dynamic Messages
Formal verification of object layout for c++ multiple inheritance
Minimal Typings in Atomic Subtyping
Controlling Interference in Ambients
Newtonian program analysis via tensor product
Barrier Inference
Complexity of Expressions Allowing Concurrency
Beginner's luck: a language for property-based generators
Cryptographically sound implementations for typed information-flow security
Memory Subsystem Performance of Programs Using Copying Garbage Collection
Static Inference of Properties of Applicative Programs
Folklore confirmed: reducible flow graphs are exponentially larger
A parametric segmentation functor for fully automatic and scalable array content analysis
Automatic patch generation by learning correct code
Casper: an efficient approach to call trace collection
Space-Time Tradeoffs for Linear Recursion
Cyclic proofs of program termination in separation logic
Extensionality and Intensionality of the Ambient Logics
Pick your contexts well: understanding object-sensitivity
Logical and Mathematical Reasoning about Imperative Programs
On Laziness and Optimality in Lambda Interpreters: Tools for Specification and Analysis
Higher-Order Concurrent Programs with Finite Communication Topology
Applications of Graph Grammar for Program Control Flow Analysis
Abstraction refinement guided by a learnt probabilistic model
High-level small-step operational semantics for transactions
Points-to analysis with efficient strong updates
A Needed Narrowing Strategy
Self-Representation in Girard's System U
Downgrading policies and relaxed noninterference
Java light is Type-Safe - Definitely
BinSlayer: accurate comparison of binary executables
What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority
Analyzing Aliases of Reference Formal Parameters
A Unified Computation Model for Functional and Logic Programming
A Complexity Theory of Grammar Problems
Treat - An Applicative Code Generator
Portable, Unobtrusive Garbage Collection for Multiprocessor Systems
Environment analysis via Delta CFA
Parametric completeness for separation theories
Or-parallel prolog execution on multicores based on stack splitting
Advice on Structuring Compilers and Proving Them Correct
Correctness of Trap-Based Breakpoint Implementations
Modular Refinement of Hierarchic Reactive Machines
Array Data-Flow Analysis and its Use in Array Privatization
Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002
A Hierarchical Basis for Reordering Transformations
Constraints: A Uniform Approach to Aliasing and Typing
A unified approach to fully lazy sharing
Interpreter Generation Using Tree Pattern Matching
Compile-Time Analysis of Parallel Programs that Share Memory
Reducing Sweep Time for a Nearly Empty Heap
Simplifying reductions
Conference Record of POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996
Projection Merging: Reducing Redundancies in Inclusion Constraint Graphs
The principles and practice of probabilistic programming
Composable Attribute Grammars: Support for Modularity in Translator Design and Implementation
Fault tolerance via idempotence
Types as models: model checking message-passing programs
The Competence/Performance Dichotomy in Programming
"Type-Completeness" as a Language Design Principle
Program Transformation in the Presence of Errors
Scaling network verification using symmetry and surgery
Autolocker: synchronization inference for atomic sections
Relational Parametricity and Units of Measure
"Look Ma, No Hashing, And No Arrays Neither"
Advanced automata minimization
Position Paper on Optimizing Compilers
Types and higher-order recursion schemes for verification of higher-order programs
Lattice-theoretic progress measures and coalgebraic model checking
A Type System for Java Bytecode Subroutines
Dependent types from counterexamples
Simple optimizations for an applicative array language for graphics processors
A Parallel Approach to Compilation
Differential Logic Programming
Effects as sessions, sessions as effects
Counterexample-guided focus
Multi-Pass Execution of Functional Logic Programs
First-class Polymorphism with Type Inference
A promising semantics for relaxed-memory concurrency
Compilers must speak properties, not just code: CAL: constraint aggregation language for declarative component-coordination
The Semantics of Local Storage, or What Makes the Free-List Free?
A Program Form Based on Data Dependency in Predicate Regions
The Global Storage Needs of a Subcomputation
Boomerang: resourceful lenses for string data
On Determining Lifetime and Aliasing of Dynamically Allocated Data in Higher-Order Functional Specifications
"Sometimes" and "Not Never" Revisited: On Branching Versus Linear Time
Constraints to Stop Higher-Order Deforestation
High-Quality Code Generation Via Bottom-Up Tree Pattern Matching
Selective memoization
Precise interprocedural analysis through linear algebra
Linear Cost is Sometimes Quadratic
Dependent Information Flow Types
On the Complexity of Beta-Reduction
Destructors, finalizers, and synchronization
Detecting Pipeline Structural Hazards Quickly
A calculus of atomic actions
Asynchronous and deterministic objects
Unified Algebras and Modules
An efficient profile-analysis framework for data-layout optimizations
Permission accounting in separation logic
Declarative data-parallel programming with the accelerator system
Program Optimization and Parallelization Using Idioms
Stratified type inference for generalized algebraic data types
Foundations for structured programming with GADTs
Subtyping arithmetical types
Compositional may-must program analysis: unleashing the power of alternation
Succinct Representation of Concurrent Trace Sets
Mathematical Semantics and Data Flow Programming
Generating precise and concise procedure summaries