Trends in functional programming : 20th International Symposium, TFP 2019, Vancouver, BC, Canada, June 12-14, 2019, Revised Selected Papers /: 20th International Symposium, TFP 2019, Vancouver, BC, Canada, June 12-14, 2019, Revised Selected Papers. (2020)

• Record Type: Book
• Other Titles: TFP 2019
• Further Information: Note: William J. Bowman, Ronald Garcia (eds.).
• Other Names: (Professor of computer science), Bowman, William J; (Professor of computer science), Garcia, Ronald; International Symposium on Trends in Functional Programming, 20th
• Contents: Intro -- 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
• Publisher Details: Cham : Springer
• Publication Date: 2020
• Extent: 1 online resource (150 pages)
• Subjects: 005.1/1; Functional programming (Computer science) -- Congresses; Logic design -- Computer programs -- Congresses; Data structures (Computer science) -- Congresses; Data structures (Computer science); Functional programming (Computer science); Logic design -- Computer programs; Electronic books; Electronic books; Conference papers and proceedings
• Languages: English
• ISBNs: 9783030471477; 3030471470
• Related ISBNs: 9783030471460
• Notes: Note: Print version record.
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.