[Lecture Notes in Computer Science] Trends in Functional Programming Volume 12053 (20th International Symposium, TFP 2019, Vancouver, BC, Canada, June 12–14, 2019, Revised Selected Papers) ||

This book constitutes the thoroughly refereed revised selected papers of the 20th International Symposium on Trends in Functional Programming, TFP 2019, held in Vancouver, Canada, in June 2019. The 6 revised full papers were selected from 11 submissions and present papers in all aspects of functional programming, taking a broad view of current and future trends in the area. It aspires to be a lively environment for presenting the latest research results, and other contributions, described in draft papers submitted prior to the symposium. -- Provided by publisher Preface Organization Contents Quotients by Idempotent Functions in Cedille 1 Introduction 2 Background 2.1 CDLE 2.2 Datatypes in Cedille 3 Quotient Types by Idempotent Functions 3.1 General Construction 3.2 Typed Equality with UIP 3.3 Natural Numbers Modulo k 3.4 Even and Odd Natural Numbers 3.5 List as Finite Set 3.6 Quotient Inductive Integers 4 Properties of Quotient Types by Idempotent Functions 4.1 Function and Property Lifting 5 Related Work 6 Conclusions References Early Experience in Teaching the Basics of Functional Language Design with a Language Type Checker 1 Background 1.1 TypeSoundnessCertifier 1.2 Our Thesis on Teaching with Language Type Checkers 2 The Details of the Course 2.1 In Class 2.2 Outside of the Class 2.3 The Evaluation 3 Report on Our Experience 3.1 Students' Mistakes 3.2 Overall Experience in Using TypeSoundnessCertifier 4 Related and Future Work 5 Conclusions References Verifying Selective CPS Transformation for Shift and Reset 1 Introduction 2 Direct-Style Terms 2.1 Purity Annotations, Types, and Terms 2.2 Substitution Relation 2.3 Frames and Evaluation Contexts 2.4 Frames and Contexts with Impure/Pure Holes 2.5 Reduction Relation 3 Selective CPS Transformation 3.1 CPS Terms 3.2 Selective CPS Transformation 4 Correctness of the Transformation 4.1 Schematic 4.2 Substitution Lemma 4.3 Continuation Reduction Lemma 4.4 Shift Lemma 4.5 Proof of the Correctness of the CPS Transformation 4.6 Notes on Agda Formalization 5 Related Work 6 Conclusion References How to Specify It! 1 Introduction 2 A Primer in Property-Based Testing 3 Our Running Example: Binary Search Trees 4 Approaches to Writing Properties 4.1 Validity Testing 4.2 Postconditions 4.3 Metamorphic Properties 4.4 Inductive Testing 4.5 Model-Based Properties 4.6 A Note on Generation 5 Bug Hunting 5.1 Bug Finding Effectiveness 5.2 Bug Finding Performance 5.3 Lessons 6 Related Work 7 Discussion A Metamorphic Properties References Type Inference for Rank 2 Gradual Intersection Types 1 Introduction 2 Rank 2 Gradual Intersection Types 3 Type System 4 Type Inference 4.1 Constraint Generation 4.2 Constraint Solving 4.3 Gradual Types 4.4 Multiple Solutions 4.5 Decidability 4.6 Soundness and Completeness 5 Conclusion A Proofs References Set Constraints, Pattern Match Analysis, and SMT 1 Introduction 2 A Set Constraint-Based Pattern Match Analysis 2.1 Match Syntax 2.2 The Underlying Type System 2.3 Annotated Types 2.4 The Analysis 3 Translating Set Constraints to SMT 3.1 A Primer in Set Constraints 3.2 Projection 3.3 Set Constraints and Monadic Logic 3.4 Monadic Logic in SMT 3.5 Reducing the Search Space 3.6 The Complete Translation 3.7 Arbitrary Boolean Combinations 4 Evaluation and Discussion References Author Index