Trends in Functional Programming: 22nd International Symposium, TFP 2021, Virtual Event, February 17–19, 2021, Revised Selected Papers (Lecture Notes in Computer Science, 12834)

Preface
Organization
Contents
Nested Parallelism, Semantics, Task-Oriented Programming
Dataset Sensitive Autotuning of Multi-versioned Code Based on Monotonic Properties
	1 Introduction
		1.1 Scope and Contributions of This Paper
	2 Background
		2.1 Brief Overview of Cuda
		2.2 Incremental Flattening
	3 Autotuning Framework
		3.1 Tuning Forests, Program Instrumentation
		3.2 Autotuning Overview
		3.3 Tuning Size-Invariant Thresholds on a Single Dataset
		3.4 Monotonicity Assumption
		3.5 Tuning Size-Variant Thresholds
	4 Experimental Validation
	5 Related Work
	6 Conclusion
	References
A Generic Back-End for Exploratory Programming
	1 Introduction
		1.1 Contributions
	2 Background
	3 Related Work
	4 Implementation
	5 Evaluation
	6 Conclusion
	References
Dynamic Editors for Well-Typed Expressions
	1 Introduction
	2 Algebraic Data Types for Queries
		2.1 Editors for ADT-Based Queries
		2.2 Evaluation of the ADT Approach
	3 Dynamic Editors
		3.1 Using Dynamic Editors
		3.2 Using the Value of a Dynamic Editor
		3.3 Overloading in Dynamic Editors
		3.4 Extendable Expressions
	4 Properly Defined DSL Identifiers
	5 Ensuring Type Safety by Phantom Types
	6 Generalized Algebraic Data Types
	7 Shallow Embedding
	8 Related Work
	9 Conclusion
	References
Modelling, Translating, Proving Functional Programs
High-Level Modelling for Typed Functional Programming
	1 Introduction
	2 Approach
	3 Modelling Context
	4 Related Work
		4.1 Mainstream Modelling Languages
		4.2 Functional Programming and Modelling
	5 Philosophical Underpinnings
	6 The Language of Mathematics
		6.1 Natural Language Structure
	7 The Bridge over the River Wittgenstein
		7.1 Proposed Basis
	8 Notation
		8.1 Design Process
		8.2 Proposed Notation
	9 Case Study
	10 Conclusion
	References
Translating Lambda Calculus into C++ Templates
	1 Introduction
	2 Related Work
	3 Template Metaprogramming
	4 Translating Lambda Calculus
	5 Translating Functional Languages
		5.1 Bindings
		5.2 Recursion
		5.3 Simple Data Types
		5.4 Complex Data Types
	6 Semantics
		6.1 Preservation
		6.2 Evaluation Order
		6.3 Compilation Errors
	7 Practical Examples
		7.1 Precomputation
		7.2 Generic Programming
	8 Conclusion
	References
ProofViz: An Interactive Visual Proof Explorer
	1 Introduction
	2 Background: Tactics vs Proof Terms
	3 A Case Study: add1+=+add1
		3.1 Inductive Proofs, Eliminators, and Equality
		3.2 Matching Tactics with Proof Terms
		3.3 Using ProofViz to Understand Induction Tactics
	4 Tactic Development with ProofViz
		4.1 Tactic Development: f-equal
		4.2 Tactic Maintenance: by-induction
	5 Implementation Details
		5.1 Using ProofViz
		5.2 Implementation
		5.3 Unresolved Challenges
	6 Related Work
	7 Evaluation, Future Work and Conclusion
	References
Author Index