MPC 2019: 13TH INTERNATIONAL CONFERENCE ON MATHEMATICS OF PROGRAM CONSTRUCTION

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

A
Agda	System F in Agda, for Fun and Profit Shallow Embedding of Type Theory Is Morally Correct
Agda formalisation	Unraveling Recursion: Compiling an IR with Recursion to System F
algebra of programming	Coding with Asymmetric Numeral Systems
arithmetic coding	Coding with Asymmetric Numeral Systems
B
blockchain	Unraveling Recursion: Compiling an IR with Recursion to System F System F in Agda, for Fun and Profit
Breadth-first algorithms	Certification of Breadth-First Algorithms by Extraction
C
canonicity	Shallow Embedding of Type Theory Is Morally Correct
Compilation	Unraveling Recursion: Compiling an IR with Recursion to System F
completeness	Completeness and Incompleteness of Synchronous Kleene Algebra
confidentiality	Experiments in Information Flow Analysis
Coq	Certification of Breadth-First Algorithms by Extraction A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning
correctness by extraction	Certification of Breadth-First Algorithms by Extraction
Cylindric algebras	Cylindric Kleene Lattices for Program Construction
D
delay monad	En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad
depth-first search	An Analysis of Repeated Graph Search
derivatives	Completeness and Incompleteness of Synchronous Kleene Algebra
E
effects	Handling Local State with Global State
equational reasoning	Handling Local State with Global State A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning
F
finite automata	Self-Certifying Railroad Diagrams, or: How to Teach Nondeterministic Finite Automata
Fixpoints	Unraveling Recursion: Compiling an IR with Recursion to System F
folds and unfolds	Coding with Asymmetric Numeral Systems
formalisation	System F in Agda, for Fun and Profit
Frames	Cylindric Kleene Lattices for Program Construction
function extensionality	Setoid Type Theory --- A Syntactic Translation
functional programming	System F in Agda, for Fun and Profit
fusion	Coding with Asymmetric Numeral Systems
G
Galois connections	Verified Self-Explaining Computation
graph search	An Analysis of Repeated Graph Search
H
Haskell	Self-Certifying Railroad Diagrams, or: How to Teach Nondeterministic Finite Automata Unraveling Recursion: Compiling an IR with Recursion to System F
I
iteration	En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad
K
Kleene algebra	Completeness and Incompleteness of Synchronous Kleene Algebra
Kleene lattices	Cylindric Kleene Lattices for Program Construction
M
metatheory	System F in Agda, for Fun and Profit
monad	A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning
monads	Handling Local State with Global State
N
non-determinism	How to Calculate with Nondeterministic Functions
nondeterminism	Handling Local State with Global State
P
parametricity	Shallow Embedding of Type Theory Is Morally Correct
probabilistic program semantics	Experiments in Information Flow Analysis
program calculation	How to Calculate with Nondeterministic Functions
program derivation	Handling Local State with Global State
program slicing	Verified Self-Explaining Computation
proof irrelevance	Setoid Type Theory --- A Syntactic Translation
Q
Quantitative Information Flow	Experiments in Information Flow Analysis
queues in functional programming	Certification of Breadth-First Algorithms by Extraction
R
recursive types	System F in Agda, for Fun and Profit
refinement	How to Calculate with Nondeterministic Functions
Refinement calculus	Cylindric Kleene Lattices for Program Construction
regular algebra	An Analysis of Repeated Graph Search
regular algebras	Self-Certifying Railroad Diagrams, or: How to Teach Nondeterministic Finite Automata
regular expressions	Self-Certifying Railroad Diagrams, or: How to Teach Nondeterministic Finite Automata
relation algebra	An Analysis of Repeated Graph Search
Relational models	Cylindric Kleene Lattices for Program Construction
reversible computation	En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad
S
Salomaa	Completeness and Incompleteness of Synchronous Kleene Algebra
security	Experiments in Information Flow Analysis
set model	Shallow Embedding of Type Theory Is Morally Correct
shallow embedding	Shallow Embedding of Type Theory Is Morally Correct A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning
Smart contracts	Unraveling Recursion: Compiling an IR with Recursion to System F System F in Agda, for Fun and Profit
SSReflect	A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning
standard model	Shallow Embedding of Type Theory Is Morally Correct
state	Handling Local State with Global State
subfactors	Self-Certifying Railroad Diagrams, or: How to Teach Nondeterministic Finite Automata
synchronous Kleene algebra	Completeness and Incompleteness of Synchronous Kleene Algebra
System F	Unraveling Recursion: Compiling an IR with Recursion to System F System F in Agda, for Fun and Profit
T
type systems	System F in Agda, for Fun and Profit
type theory	Shallow Embedding of Type Theory Is Morally Correct Setoid Type Theory --- A Syntactic Translation
U
univalence	Setoid Type Theory --- A Syntactic Translation
V
verified implementation	Verified Self-Explaining Computation

Disclaimer | Powered by EasyChair Smart Program