| Description |
1 online resource (XVI, 281 pages) : 74 illustrations |
| Series |
Lecture Notes in Computer Science, 0302-9743 ; 10818 |
|
Lecture notes in computer science ; 10818. 0302-9743
|
| Contents |
Intro -- Preface -- Organization -- Abstracts of Invited Talks -- Can Programming Be Liberated from Unidirectional Style? -- miniKanren: A Family of Languages for Relational Programming -- Building Verified Cryptographic Components Using F* -- Contents -- Formal Verification of the Correspondence Between Call-by-Need and Call-by-Name -- 1 Introduction -- 2 -Calculus and Call-by-Name Evaluation -- 3 Ariola and Felleisen's Call-by-Need -Calculus -- 4 Outline of Our Standardization-Based Proof -- 5 Formalization in Coq -- 6 Related Work -- 7 Conclusion -- References |
|
Direct Encodings of NP-Complete Problems into Horn Sequents of Multiplicative Linear Logic -- 1 Introduction -- 2 Intuitionistic Multiplicative Linear Logic, Horn Sequents, and MLL -- 2.1 Intuitionistic Multiplicative Linear Logic and Horn Sequents -- 2.2 Multiplicative Linear Logic -- 2.3 MLL Proof Nets -- 3 The Encoding of 3D MATCHING -- 3.1 Preliminaries -- 3.2 The Encoding into a Horn Sequent -- 3.3 The Correctness Proof -- 4 The Encoding of PARTITION -- 4.1 Preliminaries -- 4.2 The Encoding into a Horn Sequent -- 4.3 The Correctness Proof -- 5 Concluding Remarks -- References |
|
To SKI, Semantically -- 1 Introduction -- 2 Lambda- and SKI-calculi and the Bracket Abstraction -- 3 Semantic Translation -- 3.1 Lazy Weakening -- 4 OCaml Implementation -- 4.1 The Eta-Optimization -- 5 Compiling Real Programs -- 6 Linear algorithm -- 7 Related Work -- 8 Conclusions -- References -- Program Extraction for Mutable Arrays -- 1 Introduction -- 2 Finite Types and Finite Functions in Coq -- 2.1 A Finite Type Library-fintype -- 2.2 A Finite Function Library-finfun -- 3 Representing Mutable Arrays in Coq -- 3.1 Program Extraction for the Array State Monad |
|
3.2 Small Example: Swap Two Elements -- 4 Optimizations by an Improved Extraction Plugin -- 4.1 Destructing Large Records -- 4.2 -expansion on Case Analysis -- 5 Case Studies -- 5.1 The Union-find Data Structure -- 5.2 The Quicksort Algorithm -- 6 Related Work -- 7 Conclusion -- References -- Functional Pearl: Folding Polynomials of Polynomials -- 1 Introduction -- 2 Univariate and Multivariate Polynomials -- 2.1 Univariate Polynomial and Its Semantics -- 2.2 Bivariate Polynomials -- 2.3 Multivariate Polynomials -- 3 Operations on Polynomials -- 3.1 Rotation -- 3.2 Substitution -- 3.3 Expansion |
|
4 Compiling Polynomials -- 5 Conclusions and Related Work -- References -- A Functional Perspective on Machine Learning via Programmable Induction and Abduction -- 1 A Principled Functional Language for Machine Learning -- 2 Deduction, Induction, Abduction -- 2.1 Proofs-as-Programs for Induction -- 2.2 Proofs-as-Programs for Abduction -- 3 Programming with Induction-Abduction -- 4 The Abductive Calculus -- 5 DecML, A Functional Language for Machine Learning -- 6 Related and Further Work -- References -- Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation |
| Summary |
This book constitutes the proceedings of the 14th International Symposium on Functional and Logic Programming, FLOPS 2018, held in Nagoya, Japan, in May 2018. The 17 papers presented in this volume were carefully reviewed and selected from 41 submissions. They cover all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming focusing on topics such as functional-logic programming, re-writing systems, formal methods and model checking, program transformations and program refinements, developing programs with the help of theorem provers or SAT/SMT solvers, language design, and implementation issues |
| Subject |
Functional programming (Computer science) -- Congresses
|
|
Logic programming -- Congresses
|
|
Programming & scripting languages: general.
|
|
Computer programming -- software development.
|
|
Information technology: general issues.
|
|
Systems analysis & design.
|
|
Expert systems -- knowledge-based systems.
|
|
Software Engineering.
|
|
Computers -- Programming Languages -- General.
|
|
Computers -- Programming -- General.
|
|
Computers -- General.
|
|
Computers -- Hardware -- Handheld Devices.
|
|
Computers -- Expert Systems.
|
|
Computers -- Software Development & Engineering -- General.
|
|
Computer programming
|
|
Functional programming (Computer science)
|
|
Logic programming
|
|
Programming languages (Electronic computers)
|
|
Software engineering
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Gallagher, John P., editor
|
|
Sulzmann, Martin, editor
|
| ISBN |
9783319906867 |
|
3319906860 |
|
