PPDP'19: PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING

This page contains an index consisting of author-provided keywords.

A
abort	Exception Handling and Classical Logic
abstract machine	Crumbling Abstract Machines
administrative normal forms	Crumbling Abstract Machines
alpha-equivalence	Sharing Equality is Linear
Arrows	Functional Reactive Programming, restated
authority	Smart Contracts as Authorized Production Rules
B
binder mobility	Functional programming with lambda-tree syntax
bisimulation	Sharing Equality is Linear
C
categorical combinators	Exponential Elimination for Bicartesian Closed Categorical Combinators
classical logic	Exception Handling and Classical Logic
Compilation	Generic Encodings of Constructor Rewriting Systems
complexity	Crumbling Abstract Machines
compositional compiler correctness	Under Control: Compositionally Correct Closure Conversion with Mutable State
concurrency	Intrinsically-Typed Mechanized Semantics for Session Types
concurrent constraint programming	Spacetime Programming: A Synchronous Language for Composable Search Strategies
Confluence	Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation
constraint satisfaction problems	Spacetime Programming: A Synchronous Language for Composable Search Strategies
contracts	Smart Contracts as Authorized Production Rules
D
defunctionalization	Exponential Elimination for Bicartesian Closed Categorical Combinators
distributed consensus	Moderately Complex Paxos Made Simple: High-Level Executable Specification of Distributed Algorithms
distributed ledger	Smart Contracts as Authorized Production Rules
Domain-specific languages	Functional Reactive Programming, restated
E
EDSL	Functional Reactive Programming, restated
Elgot iteration	An Adequate While-Language for Hybrid Computation
energy	Type-Driven Verification of Extra-Functional Properties
exception handling	Exception Handling and Classical Logic
executable specification	Moderately Complex Paxos Made Simple: High-Level Executable Specification of Distributed Algorithms
exhaustive and random data generation	Property-Based Testing via Proof Reconstruction
explicit substitution	Crumbling Abstract Machines
F
first-class control	Under Control: Compositionally Correct Closure Conversion with Mutable State
formal methods	TopHat: A formal foundation for task-oriented programming
FRP	Functional Reactive Programming, restated
Functional languages	Generic Encodings of Constructor Rewriting Systems
functional programming	Functional programming with lambda-tree syntax
functional programming language	TopHat: A formal foundation for task-oriented programming
Functional Reactive Programming	Functional Reactive Programming, restated
G
guarded iteration	An Adequate While-Language for Hybrid Computation
H
high-level specification	Moderately Complex Paxos Made Simple: High-Level Executable Specification of Distributed Algorithms
higher-order abstract syntax	Functional programming with lambda-tree syntax
hybrid monad	An Adequate While-Language for Hybrid Computation
I
idris	Type-Driven Verification of Extra-Functional Properties
Inductive Theorem Proving	Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation
Infinite List	Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation
Interactive refutation	Relational Symbolic Execution
Intuitionistic Propositional Logic	Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus
K
Kripke logical relations	Under Control: Compositionally Correct Closure Conversion with Mutable State
L
lambda calculus	Exception Handling and Classical Logic
lambda tree syntax	Property-Based Testing via Proof Reconstruction
lambda-calculus	Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus Crumbling Abstract Machines Sharing Equality is Linear
lambda-tree syntax	Functional programming with lambda-tree syntax
Language design	Relational Symbolic Execution
logic programming	Property-Based Testing via Proof Reconstruction
M
mechanized metatheory	Intrinsically-Typed Mechanized Semantics for Session Types
message-history queries	Moderately Complex Paxos Made Simple: High-Level Executable Specification of Distributed Algorithms
Monad	Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus
multi-language semantics	Under Control: Compositionally Correct Closure Conversion with Mutable State
mutable state	Under Control: Compositionally Correct Closure Conversion with Mutable State
N
Non-termination	Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation
Normalization	Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus
normalization by evaluation	Exponential Elimination for Bicartesian Closed Categorical Combinators
O
open terms	Crumbling Abstract Machines
operational semantics	TopHat: A formal foundation for task-oriented programming
P
Pattern matching	Generic Encodings of Constructor Rewriting Systems
Paxos	Moderately Complex Paxos Made Simple: High-Level Executable Specification of Distributed Algorithms
Polarized Logic	Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus
program generation	TopHat: A formal foundation for task-oriented programming
Program Transformation	Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation
proof certificates	Property-Based Testing via Proof Reconstruction
proof checking	Property-Based Testing via Proof Reconstruction
Proof of correctness	Relational Symbolic Execution
property based testing	Property-Based Testing via Proof Reconstruction
R
Reactive Programming	Functional Reactive Programming, restated
Relational reasoning	Relational Symbolic Execution
Rule based languages	Generic Encodings of Constructor Rewriting Systems
S
search strategy	Spacetime Programming: A Synchronous Language for Composable Search Strategies
security	Type-Driven Verification of Extra-Functional Properties
semantics	Intrinsically-Typed Mechanized Semantics for Session Types Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus Smart Contracts as Authorized Production Rules
session types	Intrinsically-Typed Mechanized Semantics for Session Types
sharing	Sharing Equality is Linear
subformula property	Exponential Elimination for Bicartesian Closed Categorical Combinators
Sufficient Completeness	Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation
Symbolic execution	Relational Symbolic Execution
Synchronous dataflow	Functional Reactive Programming, restated
synchronous programming	Spacetime Programming: A Synchronous Language for Composable Search Strategies
T
task oriented programming	TopHat: A formal foundation for task-oriented programming
Term Rewriting	Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation
Term rewriting systems	Generic Encodings of Constructor Rewriting Systems
time	Type-Driven Verification of Extra-Functional Properties
typed closure conversion	Under Control: Compositionally Correct Closure Conversion with Mutable State
types	Type-Driven Verification of Extra-Functional Properties
V
verification	Type-Driven Verification of Extra-Functional Properties
W
workflow modelling	TopHat: A formal foundation for task-oriented programming
Z
Zeno behaviour	An Adequate While-Language for Hybrid Computation

Disclaimer | Powered by EasyChair Smart Program