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

Description

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