yusuke1997/dblp-id-title huggingface dataset:
Loops in Combinator-Based Compilers
Actor Induction and Meta-Evaluation
Flexible types: robust type inference for first-class polymorphism
A Compilation Method for ML-Style Polymorphic Record Calculi
An executable formal semantics of C with applications
Sound type-dependent syntactic language extension
Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978
Ur/Web: A Simple Model for Programming the Web
On Linearizing Parallel Code
Verifying distributed systems: the operational approach
On the power of coercion abstraction
A Unified Treatment of Flow Analysis in Higher-Order Languages
Principled parsing for indentation-sensitive languages: revisiting landin's offside rule
Bisimulation for quantum processes
Semantics and Correctness of a Query Language Translation
Manifest Contracts for Datatypes
Denotational Semantics Using an Operationally-Based Term Model
POPL 2000, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, January 19-21, 2000
An abstract interpretation-based framework for software watermarking
Partial Order Programming
The essence of Reynolds
Back to the future: revisiting precise program verification using SMT solvers
Procedure Linkage Optimization
A Functional Theory of Local Names
The Universality of Data Retrieval Languages
Non-Syntactic Attribute Flow in Language Based Editors
Declarative aspects of memory management in the concurrent collections parallel programming model
Labelled Precedence Parsing
Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, USA, January 1993
A compiler technique for improving whole-program locality
Guardians and Actions: Linguistic Support for Robust, Distributed Programs
Probabilistic coherence spaces are fully abstract for probabilistic PCF
Transactors: a programming model for maintaining globally consistent distributed state in unreliable environments
POPL '99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999
Once Upon a Polymorphic Type
Proceedings of the POPL 2005 Workshop on Issues in the Theory of Security, WITS 2005, Long Beach, California, USA, January 10-11, 2005
Representation Independence and Data Abstraction
"Type" Is Not A Type
Streaming transducers for algorithmic verification of single-pass list-processing programs
Learning nominal automata
Separation Constraint Partitioning - A New Algorithm for Partitioning Non-strict Programs into Sequential Threads
Parallelizing constraint programs
Carrier Arrays: An Idiom-Preserving Extension to APL
Application of Lattice Algebra to Loop Optimization
Environments as First Class Objects
The strength of non-size increasing computation
Decidability of inferring inductive invariants
Modalities for Model Checking: Branching Time Strikes Back
Parallelization in Calculational Forms
Memoryful geometry of interaction II: recursion and adequacy
Classical BI: a logic for reasoning about dualising resources
Reduction in Strength of High Level Operations
Stack inspection: theory and variants
Communicating quantum processes
Breaking through the normalization barrier: a self-interpreter for f-omega
Decidability and proof systems for language-based noninterference relations
Constraining-Unification and the Programming Language Unicorn
Colored local type inference
Efficient Applicative Data Types
First Order Programming Logic
Higher-Order Functors with Transparent Signatures
Extensible encoding of type hierarchies
Semantics-Directed Code Generation
Optimal dynamic partial order reduction
Determining the Idle Time of a Tiling
Extensions for Multi-Module Records in Conventional Programming Languages
Breaking the GPU programming barrier with the auto-parallelising SAC compiler
An Indeterminate Constructor for Applicative Programming
Binding as sets of scopes
Abstract effects and proof-relevant logical relations
Kernel mode API spectroscopy for incident response and digital forensics
Local Type Inference
Tabular: a schema-driven probabilistic programming language
A fixpoint calculus for local and global program flows
Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach
Optimal-Time Incremental Semantic Analysis for Syntax-Directed Editors
Unboxed Objects and Polymorphic Typing
Inverse Currying Transformation on Attribute Grammars
Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, USA, January 1980
A Program Development Tool
Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 19-22, 1992
Temporal Logic Programming is Complete and Expressive
Authentication Primitives and Their Compilation
Modules, abstraction, and parametric polymorphism
Conversion of Control Dependence to Data Dependence
Type-preserving garbage collectors
A Compact, Machine-Independent Peephole Optimizer
Sound input filter generation for integer overflow errors
A Modal Analysis of Staged Computation
Coarse-grained transactions
Program Fragments, Linking, and Modularization
A verified information-flow architecture
Analysis of Pointer Rotation
Parallel Beta Reduction is not Elementary Recursive
Quasi-Static Typing
Test Data as an Aid in Proving Program Correctness
The Pi-calculus in Direct Style
On Proving Inductive Properties of Abstract Data Types
A Provably Time-Efficient Parallel Implementation of Full Speculation
On coinductive equivalences for higher-order probabilistic functional programs
Faster Checking of Software Specifications by Eliminating Isomorphs
Proceedings of the Programming Languages Mentoring Workshop, PLMW@POPL 2015, Mumbai, India, January 14, 2015
Message of thanks: on the receipt of the 2011 ACM SIGPLAN distinguished achievement award
A Comprehensive Study of the Complexity of Multiparty Interaction
Model checking for symbolic-heap separation logic with inductive predicates
30 years of research and development around Coq
Programming language methods in computer security
A Mechanically Certified Theorem about Optimal Concurrency of Sorting Networks
Focusing and higher-order abstract syntax
Termination of Probabilistic Concurrent Programs
Bisimilarity for a First-Order Calculus of Objects with Subtyping
On the Complexity of LR(k) Testing
Applications of High-Level Control Flow
Paths: An Abstract Alternative to Pointers
Parallelism in Logic Programs
Finding the Source of Type Errors
Ogre and Pythia: an invariance proof method for weak consistency models
Strictness Analysis Aids Time Analysis
The m-calculus: a higher-order distributed process calculus
Multiple facets for dynamic information flow
Structural Semantics for Polymorphic Data Types
Automatic Construction of Sparse Data Flow Evaluation Graphs
A syntactic approach to eta equality in type theory
Ypnos: declarative, parallel structured grid programming
Dependence Flow Graphs: An Algebraic Approach to Program Dependencies
Streaming big data with self-adjusting computation
On the Unification of Data and Program Abstraction in Ada
JavaScript instrumentation for browser security
Dynamic inference of static types for ruby
Modeling abstract types in modules with open existential types
Parameterized Types for Java
Data Flow Analysis of Communicating Processes
Overhauling SC atomics in C11 and OpenCL
Inductive Definitions, Semantics and Abstract Interpretation
Inference of Polymorphic and Conditional Strictness Properties
A New Strategy for Code Generation - The General Purpose Optimizing Compiler
Pure patterns type systems
Efficient Tree Pattern Matching: An Aid to Code Generation
Logic-flow analysis of higher-order programs
Syntactic Control of Interference
Exploiting prolific types for memory management and optimizations
Goal-Directed Program Transformation
A compiler and run-time system for network programming languages
Safe Type Checking in a Statically-Typed Object-Oriented Programming Language
Dynamic race detection for C++11
An Efficient Way to Find Side Effects of Procedure Calls and Aliases of Variables
Abstractions from tests
Specifying Kerberos 5 cross-realm authentication
Logical relations for fine-grained concurrency
Controlling loops in parallel mercury code
Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation
From POPL to the classroom and back
Nondeterminism in Logics of Programs
Data Flow Analysis is Model Checking of Abstract Interpretations
Towards nominal computation
Region-based shape analysis with tracked locations
Integrating Non-Interfering Versions of Programs
A model of cooperative threads
Conference Record of the Second ACM Symposium on Principles of Programming Languages, Palo Alto, California, USA, January 1975
Proceedings of the 3rd ACM SIGPLAN Program Protection and Reverse Engineering Workshop 2014, PPREW 2014, January 25, 2014, San Diego, CA, USA
Certified assembly programming with embedded code pointers
Type inference for datalog with complex type hierarchies
A logic you can count on
Incremental execution of transformation specifications
Time and Space Profiling for Non-Strict Higher-Order Functional Languages
Is "Just in Time" = "Better Late than Never"?
Applicative Functors and Fully Transparent Higher-Order Modules
Type theory in type theory using quotient inductive types
Synthesis of reactive controllers for hybrid systems (keynote)
Multivariate amortized resource analysis
Gradual refinement types
Code Generation for Expressions with Common Subexpressions
Compilers and Staging Transformations
The intensional content of Rice's theorem
Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol
On flow-sensitive security types
A Proper Extension of ML with an Effective Type-Assignment
Feedback-directed barrier optimization in a strongly isolated STM
Constraint Systems for Useless Variable Elimination
Paths vs. Trees in Set-Based Program Analysis
Synthesis of Concurrent Systems with Many Similar Sequential Processes
Bitwidth aware global register allocation
'Cause I'm strong enough: reasoning about consistency choices in distributed systems
Nomadic pict: correct communication infrastructure for mobile computation
Maximal specification synthesis
A Parallel Language and its Compilation to Multiprocessor Machines or VLSI
A Less Dynamic Memory Allocation Scheme for Algol-like Languages
Discovering affine equalities using random interpretation
Type Definitions with Parameters
Analysis of recursively parallel programs
Linear types for computational effects
An abstract interpretation framework for termination
Algorithmic Aspects of Type Inference with Subtypes
Paragon: Novel Uses of Type Hierarchies for Data Abstraction
On the Orthogonality of Assignments and Procedures in Algol
The semantics of progress in lock-based transactional memory
Formally Optimal Boxing
Default Timed Concurrent Constraint Programming
Higher Inductive Types as Homotopy-Initial Algebras
Type directed compilation of row-typed algebraic effects
A theory of effects and resources: adjunction models and polarised calculi
The Call-by-Need Lambda Calculus
Parallel functional arrays
Mining specifications
Mode Modules as Representations of Domains
Data-Parallel String-Manipulating Programs
Systems biology, models, and concurrency
Static and user-extensible proof checking
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
Implementation of an Interpreter for Abstract Equations
Complexity of Bidirectional Data Flow Analysis
The size-change principle for program termination
Enhancing modular OO verification with separation logic
Complexity of pattern-based verification for multithreaded programs
Proceedings of the 2nd ACM SIGPLAN Program Protection and Reverse Engineering Workshop 2013, PPREW@POPL 2013, January 26, 2013, Rome, Italy
Garbage Collecting the World
Relaxed-memory concurrency and verified compilation
Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems
Dynamically Bypassing Copy Rule Chains in Attribute Grammars
Polymorphism, subtyping, and type inference in MLsub
Formal certification of code-based cryptographic proofs
Automata-Driven Indexing of Prolog Clauses
Formalization of Exel
Making Asynchronous Parallelism Safe for the World
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
An Efficient Method of Computing Static Single Assignment Form
High Level Reading and Data Structure Compilation
Skinny and Fleshy Failures of Relative Completeness
Towards the Essence of Hygiene
Parametric polymorphism for XML
Even Simple Programs are Hard to Analyze
Much ado about two (pearl): a pearl on parallel prefix computation
On Characterizing the Data Access Complexity of Programs
HALO: haskell to logic through denotational semantics
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016
Bounded Fixed Point Iteration
Optimally Profiling and Tracing Programs
Mixed-size concurrency: ARM, POWER, C/C++11, and SC
An Efficient Hybrid Algorithm for Incremental Data Flow Analysis
PLAN2D - Syntactic Analysis of Precedence Graph Grammars
Backpack: retrofitting Haskell with interfaces
Axiomatic Definability and Completeness for Recursive Programs
Verifying liveness for asynchronous programs
Cultivating research taste (illustrated via a journey in program synthesis research)
Symbolic Programming Analysis in Almost Linear Time
Decentralizing SDN Policies
Clowns to the left of me, jokers to the right (pearl): dissecting data structures
A very modal model of a modern, major, general type system
Assessing security threats of looping constructs
Formal Program Testing
Description-Driven Code Generation using Attribute Grammars
Axiomatic Definitions of Programming Languages, II
Symbolic Evaluation and the Global Value Graph
Continuity analysis of programs
Monad Transformers and Modular Interpreters
Completion Semantics, Interpreter Generation
Computer Experiments with the Reve Term Rewriting System Generator
Modelling the ARMv8 architecture, operationally: concurrency and ISA
Second-Order Unification and Type Inference for Church-Style Polymorphism
Environmental acquisition revisited
Automatic Generation of Machine Specific Code Optimizers
Fast Interprocedural Class Analysis
Typed Closure Conversion
Low-level liquid types
PASTHA: parallelizing stencil calculations in Haskell
An Extension of Standard ML Modules with Subtyping and Inheritance
Parametric Program Slicing
Modeling Continuations without Continuations
Battery transition systems
Higher-Order unCurrying
The Revival Transformation
Correctness of Monadic State: An Imperative Call-by-Need Calculus
Equations, Contractions, and Unique Solutions
Locality in Software Systems
Automatic Generation and Management of Interprocedural Program Analyses
Coupling proofs are probabilistic product programs
A virtual class calculus
Algorithms for algebraic path properties in concurrent systems of constant treewidth components
Fencing off go: liveness and safety for channel-based programming
Experience with an Applicative String Processing Language
A Relationship Between Abstract Interpretation and Projection Analysis
Matchmaker: An Interface Specification Language for Distributed Processing
Generalized Common Subexpressions in Very High Level Languages
Automatically generating instruction selectors using declarative machine descriptions
Reasoning About Nonatomic Operations
The Program Dependence Graph and Vectorization
Automatic Generation of Efficient Evaluators for Attribute Grammars
Toward a verified relational database management system
On the Complexity of Escape Analysis
Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
A shape analysis for optimizing parallel graph programs
Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview
Verifying Reachability Invariants of Linked Structures
Scalable formal design methods for asynchronous VLSI
Combining static analysis with probabilistic models to enable market-scale Android inter-component analysis
Search and Imperative Programming
Behavioral Equivalence in the Polymorphic Pi-calculus
Secure safe ambients
Synthesis of Resource Invariants for Concurrent Programs
Correct Flow Analysis in Continuation Semantics
Separation logic for weak memory models
Proceedings of the POPL 2010 Workshop on Declarative Aspects of Multicore Programming, DAMP 2010, Madrid, Spain, January 19, 2010
Safe nondeterminism in a deterministic-by-default parallel language
Optimal Code Selection in DAGs
Incremental Compilation via Partial Evaluation
Bisimulation Through Probabilistic Testing
Compiling Path Expressions into VLSI Circuits
Scheduling Arithmetic and Load Operations in Parallel with No Spilling
Query-guided maximum satisfiability
Verifying safety properties of concurrent Java programs using 3-valued logic
Transformational Programming - Applications to Algorithms and Systems
Simple relational correctness proofs for static analyses and program transformations
Interactive proofs in higher-order concurrent separation logic
A Type-Theoretic Approach to Higher-Order Modules with Sharing
Meta-level features in an industrial-strength theorem prover
A Semantics-Directed Compiler Generator
Modeling Concurrency with Geometry
Actor Semantics of Planner-73
Types as Abstract Interpretations
The geometry of parallelism: classical, probabilistic, and quantum effects
Runtime Enforcement of Security Policies on Black Box Reactive Programs
Proceedings of the 2013 Workshop on Data Driven Functional Programming, DDFP 2013, Rome, Italy, January 22, 2013
Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011
Proving that non-blocking algorithms don't block
Paging as a "Language Processing" Task
Binding Performance at Language Design Time
Lock allocation
Constant Propagation with Conditional Branches
Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005
Generative unbinding of names
The SLam Calculus: Programming with Secrecy and Integrity
Closurize and Concentrate
The Geometry of Optimal Lambda Reduction
Analyzing divergence in bisimulation semantics
SMO: an integrated approach to intra-array and inter-array storage optimization
Using Dependent Types to Express Modular Structure
A Calculus for Assignments in Higher-Order Languages
From symptom to cause: localizing errors in counterexample traces
A relationally parametric model of dependent type theory
Computation of Aliases and Support Sets
Inferring authentication tags
A High-Level Approach to Computer Document Formatting
Specialization of CML message-passing primitives
Conference Record of the ACM Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, October 1973
Dynamic partial-order reduction for model checking software
Confluences in programming languages research (keynote)
Messages as Active Agents
Automatic Data Structure Selection in SETL
Formalization of generics for the .NET common language runtime
Interprocedural compatibility analysis for static object preallocation
Analysis of a Simple Algorithm for Global Flow Problems
Self-certification: bootstrapping certified typecheckers in F* with Coq
Type Checking Type Classes
A Type System for Expressive Security Policies
Synthesis of biological models from mutation experiments
A Simple, Comprehensive Type System for Java Bytecode Subroutines
POPL: The First Ten Years, Proceedings Compenium 1973-1983, CDROM
S-Net for multi-memory multicores
Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints
Expressional Loops
Program Improvement by Internal Specialization
Computer Architectures and Programming Models for Scalable Parallel Computing
Verifying higher-order functional programs with pattern-matching algebraic data types
Eliminating Redundant Object Code
The Scala experiment: can we provide better language support for component systems?
The Essence of ML
Quantitative abstraction refinement
A Core Calculus of Dependency
PSync: a partially synchronous language for fault-tolerant distributed algorithms
Stratified operational semantics for safety and correctness of the region calculus
The semantics of power and ARM multiprocessor machine code
The ramifications of sharing in data structures
Conference Record of the Eighth Annual ACM Symposium on Principles of Programming Languages, Williamsburg, Virginia, USA, January 1981
A theorem prover for Boolean BI
An Algebra of Relations for Machine Computation
The type discipline of behavioral separation
Small bisimulations for reasoning about higher-order imperative programs
Limitations of Synchronous Communication with Static Process Structure in Languages for Distributed Computing
Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated
Parallel Programming With Coordination Structures
Automatic Data Structure Choice in a Language of Very High Level
Predicate abstraction for software verification
Generating a Compiler for a Lazy Language by Partial Evaluation
Data Flow Analysis of Applicative Programs Using Minimal Function Graphs
Implementation of the Typed Call-by-Value lambda-Calculus using a Stack of Regions
Solving Shape-Analysis Problems in Languages with Destructive Updating
An Extended Form of Must Alias Analysis for Dynamic Allocation
Modular type classes
Language constructs for transactional memory
Statically checking confidentiality via dynamic labels
Compositional Analysis of Modular Logic Programs
The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014
An Interprocedural Data Flow Analysis Algorithm
Staged allocation: a compositional technique for specifying and implementing procedure calling conventions
A mechanized semantics for C++ object construction and destruction, with applications to resource management
A language for automatically enforcing privacy policies
Higher-order functional reactive programming in bounded space
The sequential semantics of producer effect systems
Smart Recompilation
Global value numbering using random interpretation
Automating Repetitive Tasks for the Masses
Partial Evaluation as a Means for Inferencing Data Structures in an Applicative Language: A Theory and Implementation in the Case of Prolog
Structural Decidable Extensions of Bounded Quantification
Demand-driven alias analysis for C
Efficient Temporal Reasoning
Precise interprocedural analysis using random interpretation
Typing Algorithm in Type Theory with Inheritance
Semi-sparse flow-sensitive pointer analysis
Copy Elimination in Functional Languages
Blame for all
Mobile values, new names, and secure communication
Code Generation and Reorganization in the Presence of Pipeline Constraints
A Collecting Interpretation of Expressions (Without Powerdomains)
Proof search for propositional abstract separation logics via labelled sequents
Objective ML: A Simple Object-Oriented Extension of ML
Multi-DaC programming model: a variant of multi-BSP model for divide-and-conquer algorithms
Theoretical and Emperical Studies on Using Program Mutation to Test the Functional Correctness of Programs
Thread modularity at many levels: a pearl in compositional verification
Delay-bounded scheduling
Bigraphs and transitions
K-Java: A Complete Semantics of Java
From control effects to typed continuation passing
Completeness and Incompleteness of Trace-Based Network Proof Systems
On verifying causal consistency
Strict Deterministic Versus LR(0) Parsing
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
Resourceable, retargetable, modular instruction selection using a machine-independent, type-based tiling of low-level intermediate code