Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
PLPV '11 : proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification : January 29, 2011, Austin, Texas, USA
| PLPV '11 : proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification : January 29, 2011, Austin, Texas, USA |
| Autore | Jhala Ranjit |
| Pubbl/distr/stampa | [Place of publication not identified], : ACM, 2011 |
| Descrizione fisica | 1 online resource (62 pages) |
| Collana | ACM Conferences |
| Soggetto topico |
Engineering & Applied Sciences
Computer Science |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Altri titoli varianti |
Programming Languages Meets Program Verification'11 : proceedings of the 5th Association for Computing Machinery workshop on Programming Languages Meets Program Verification : January 29, 2011, Austin, Texas, United States of America
Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification POPL '11 the 38th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Austin, TX, USA - January 26 - 28, 2011 |
| Record Nr. | UNINA-9910376024003321 |
Jhala Ranjit
|
||
| [Place of publication not identified], : ACM, 2011 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Trends in functional programming : 23rd International Symposium, TFP 2022, virtual event, March 17-18, 2022, revised selected papers / / edited by Wouter Swierstra, Nicolas Wu
| Trends in functional programming : 23rd International Symposium, TFP 2022, virtual event, March 17-18, 2022, revised selected papers / / edited by Wouter Swierstra, Nicolas Wu |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (200 pages) |
| Disciplina | 910.5 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Functional programming (Computer science) |
| ISBN | 3-031-21314-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Project Paper: Embedding Generic Monadic Transformer into Scala -- 1 Introduction -- 2 Embedding Generic Monadic Cps Transform into Scala -- 2.1 Monads Parametrization -- 2.2 Translation of Higher-Order Functions -- 2.3 Call-Chain Substitutions -- 2.4 Automatic Coloring -- 3 Related Work -- 4 Conclusion and Further Work -- References -- Towards a Language for Defining Reusable Programming Language Components -- 1 Introduction -- 2 CS by Example -- 2.1 Data Types and Functions -- 2.2 Effects and Handlers -- 2.3 Order of Evaluation, Suspension, and Enactment -- 2.4 Modules and Imports -- 2.5 Composable Data Types and Functions -- 3 Defining Reusable Language Components in CS -- 3.1 A Signature for Reusable Components -- 3.2 A Language Component for Arithmetic Expressions -- 3.3 Implementing Functions as a Reusable Effect -- 3.4 Example Usage -- 4 Related Work -- 5 Future Work -- 6 Conclusion -- References -- Deep Embedding with Class -- 1 Introduction -- 1.1 Research Contribution -- 2 Deep Embedding -- 3 Shallow Embedding -- 3.1 Tagless-Final Embedding -- 4 Lifting the Backends -- 5 Existential Data Types -- 5.1 Unbraiding the Semantics from the Data -- 6 Transformation Semantics -- 6.1 Convolution -- 6.2 Pattern Matching -- 6.3 Chaining Semantics -- 7 Generalised Algebraic Data Types -- 8 Conclusion -- 9 Related Work -- A Appendix -- A.1 Data Type Definitions -- A.2 Smart Constructors -- A.3 Semantics Classes and Data Types -- A.4 GDict instances -- A.5 Evaluator Instances -- A.6 Printer Instances -- A.7 Optimisation Instances -- References -- Understanding Algebraic Effect Handlers via Delimited Control Operators -- 1 Introduction -- 2 S0: A Calculus of Shift0 and Dollar -- 3 h: A Calculus of Effect Handlers -- 4 Adding and Removing the Return Clause -- 4.1 Translating Between Dollar and Reset0.
4.2 Translating Between Handlers with and Without Return Clause -- 4.3 Correctness -- 5 Deriving a CPS Translation -- 5.1 CPS Translation of Shift0 and Dollar -- 5.2 CPS Translation of Effect Handlers -- 5.3 Macro Translation from h to S0 -- 5.4 Composing Macro and CPS Translations -- 6 Deriving a Type System from the CPS Translation -- 6.1 Type System of Shift0 and Dollar -- 6.2 Type System of Effect Handlers -- 6.3 Applying the CPS Approach -- 6.4 Soundness -- 7 Related Work -- 8 Conclusion and Future Perspectives -- References -- Reducing the Power Consumption of IoT with Task-Oriented Programming -- 1 Introduction -- 1.1 Research Contribution -- 2 Task-Oriented Programming -- 2.1 mTask -- 3 Energy Efficient IoT Nodes -- 4 Scheduling Tasks Efficiently -- 4.1 Evaluation Interval -- 4.2 Basic Refresh Rates -- 4.3 Deriving Refresh Rates -- 4.4 User Defined Refresh Rates -- 5 Running Tasks on Interrupts -- 6 Implementing Refresh Rates -- 7 Scheduling Tasks -- 8 Resulting Power Reductions -- 8.1 Power Saving -- 9 Related Work -- 10 Conclusion -- References -- Semantic Equivalence of Task-Oriented Programs in TopHat -- 1 Introduction -- 2 The TopHat Language -- 2.1 Editors -- 2.2 Sequential Composition -- 2.3 Parallel Composition -- 2.4 Observations -- 2.5 Semantics -- 3 Contextual Equivalence -- 4 Expression Equivalence -- 5 Task Conditions -- 5.1 Failing Tasks -- 5.2 Finished Tasks -- 5.3 Stuck Tasks -- 5.4 Running Tasks -- 6 Task Equivalence -- 7 Laws on Tasks -- 8 Conclusions -- A Appendix -- A.1 Failing -- A.2 Inputs -- A.3 Value -- References -- Algorithm Design with the Selection Monad -- 1 Introduction -- 2 Selection Functions -- 2.1 Pairs of Selection Functions -- 2.2 Password Example -- 2.3 Iterated Product of Selection Functions -- 2.4 Dependently Typed Version -- 2.5 Extended Password Example -- 2.6 Selection Functions Form a Monad. 2.7 History-Dependent Product of Selection Functions -- 2.8 Efficiency Drawbacks of This Implementation -- 3 Greedy Algorithms -- 4 Examples of Greedy Algorithms -- 4.1 Password Example -- 4.2 Prim's Algorithm -- 4.3 Greedy Graph Walking -- 5 Correctness -- 6 Limited Lookahead -- 6.1 Graph Example -- 7 Iterated Product -- 7.1 Examples -- 8 Conclusion and Future Work -- A Proof that Product Equals Sequence -- References -- Sound and Complete Type Inference for Closed Effect Rows -- 1 Introduction -- 2 Motivation -- 2.1 Algebraic Effects and Handlers -- 2.2 Naive Hindley-Milner Type Inference with Algebraic Effects and Handlers -- 2.3 Type Inference with open and close -- 3 Implicitly Typed Calculus for Algebraic Effects and Handlers -- 3.1 Syntax -- 3.2 Declarative Type Inference Rules -- 4 Syntax-Directed Type Inference Rules -- 4.1 Type Substitution -- 4.2 Type Ordering -- 4.3 Inference Rules with open and close -- 4.4 Principles on the Use of [let] Rule -- 4.5 Fragility of [let] Rule -- 5 Type Inference Algorithm -- 5.1 Auxiliary Functions -- 5.2 Unification Algorithm -- 5.3 Type Inference Algorithm -- 6 Related Work -- 7 Conclusion and Future Work -- A System F + restrict -- B Type-Directed Translation to System F+restrict -- References -- Towards Efficient Adjustment of Effect Rows -- 1 Introduction -- 2 Overview -- 2.1 Effect Handlers -- 2.2 Evidence Passing Semantics and Row-Based Effect System -- 2.3 Effect Type Adjustment for Function Types -- 2.4 Motivating Open Floating -- 3 System Fpwo -- 3.1 Syntax -- 3.2 Dynamic Semantics -- 3.3 Static Semantics -- 3.4 Effect Rows and Closed Prefix Relation -- 4 Open Floating -- 4.1 Design of Algorithm -- 4.2 Organization of Definition -- 4.3 The Definition -- 4.4 Example -- 5 Evaluation -- 5.1 Ideal Case -- 5.2 Failure Case -- 6 Future Work -- 7 Related Work -- 8 Conclusion -- References -- Author Index. |
| Record Nr. | UNINA-9910639887703321 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Trends in functional programming : 23rd International Symposium, TFP 2022, virtual event, March 17-18, 2022, revised selected papers / / edited by Wouter Swierstra, Nicolas Wu
| Trends in functional programming : 23rd International Symposium, TFP 2022, virtual event, March 17-18, 2022, revised selected papers / / edited by Wouter Swierstra, Nicolas Wu |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (200 pages) |
| Disciplina | 910.5 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Functional programming (Computer science) |
| ISBN | 3-031-21314-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Project Paper: Embedding Generic Monadic Transformer into Scala -- 1 Introduction -- 2 Embedding Generic Monadic Cps Transform into Scala -- 2.1 Monads Parametrization -- 2.2 Translation of Higher-Order Functions -- 2.3 Call-Chain Substitutions -- 2.4 Automatic Coloring -- 3 Related Work -- 4 Conclusion and Further Work -- References -- Towards a Language for Defining Reusable Programming Language Components -- 1 Introduction -- 2 CS by Example -- 2.1 Data Types and Functions -- 2.2 Effects and Handlers -- 2.3 Order of Evaluation, Suspension, and Enactment -- 2.4 Modules and Imports -- 2.5 Composable Data Types and Functions -- 3 Defining Reusable Language Components in CS -- 3.1 A Signature for Reusable Components -- 3.2 A Language Component for Arithmetic Expressions -- 3.3 Implementing Functions as a Reusable Effect -- 3.4 Example Usage -- 4 Related Work -- 5 Future Work -- 6 Conclusion -- References -- Deep Embedding with Class -- 1 Introduction -- 1.1 Research Contribution -- 2 Deep Embedding -- 3 Shallow Embedding -- 3.1 Tagless-Final Embedding -- 4 Lifting the Backends -- 5 Existential Data Types -- 5.1 Unbraiding the Semantics from the Data -- 6 Transformation Semantics -- 6.1 Convolution -- 6.2 Pattern Matching -- 6.3 Chaining Semantics -- 7 Generalised Algebraic Data Types -- 8 Conclusion -- 9 Related Work -- A Appendix -- A.1 Data Type Definitions -- A.2 Smart Constructors -- A.3 Semantics Classes and Data Types -- A.4 GDict instances -- A.5 Evaluator Instances -- A.6 Printer Instances -- A.7 Optimisation Instances -- References -- Understanding Algebraic Effect Handlers via Delimited Control Operators -- 1 Introduction -- 2 S0: A Calculus of Shift0 and Dollar -- 3 h: A Calculus of Effect Handlers -- 4 Adding and Removing the Return Clause -- 4.1 Translating Between Dollar and Reset0.
4.2 Translating Between Handlers with and Without Return Clause -- 4.3 Correctness -- 5 Deriving a CPS Translation -- 5.1 CPS Translation of Shift0 and Dollar -- 5.2 CPS Translation of Effect Handlers -- 5.3 Macro Translation from h to S0 -- 5.4 Composing Macro and CPS Translations -- 6 Deriving a Type System from the CPS Translation -- 6.1 Type System of Shift0 and Dollar -- 6.2 Type System of Effect Handlers -- 6.3 Applying the CPS Approach -- 6.4 Soundness -- 7 Related Work -- 8 Conclusion and Future Perspectives -- References -- Reducing the Power Consumption of IoT with Task-Oriented Programming -- 1 Introduction -- 1.1 Research Contribution -- 2 Task-Oriented Programming -- 2.1 mTask -- 3 Energy Efficient IoT Nodes -- 4 Scheduling Tasks Efficiently -- 4.1 Evaluation Interval -- 4.2 Basic Refresh Rates -- 4.3 Deriving Refresh Rates -- 4.4 User Defined Refresh Rates -- 5 Running Tasks on Interrupts -- 6 Implementing Refresh Rates -- 7 Scheduling Tasks -- 8 Resulting Power Reductions -- 8.1 Power Saving -- 9 Related Work -- 10 Conclusion -- References -- Semantic Equivalence of Task-Oriented Programs in TopHat -- 1 Introduction -- 2 The TopHat Language -- 2.1 Editors -- 2.2 Sequential Composition -- 2.3 Parallel Composition -- 2.4 Observations -- 2.5 Semantics -- 3 Contextual Equivalence -- 4 Expression Equivalence -- 5 Task Conditions -- 5.1 Failing Tasks -- 5.2 Finished Tasks -- 5.3 Stuck Tasks -- 5.4 Running Tasks -- 6 Task Equivalence -- 7 Laws on Tasks -- 8 Conclusions -- A Appendix -- A.1 Failing -- A.2 Inputs -- A.3 Value -- References -- Algorithm Design with the Selection Monad -- 1 Introduction -- 2 Selection Functions -- 2.1 Pairs of Selection Functions -- 2.2 Password Example -- 2.3 Iterated Product of Selection Functions -- 2.4 Dependently Typed Version -- 2.5 Extended Password Example -- 2.6 Selection Functions Form a Monad. 2.7 History-Dependent Product of Selection Functions -- 2.8 Efficiency Drawbacks of This Implementation -- 3 Greedy Algorithms -- 4 Examples of Greedy Algorithms -- 4.1 Password Example -- 4.2 Prim's Algorithm -- 4.3 Greedy Graph Walking -- 5 Correctness -- 6 Limited Lookahead -- 6.1 Graph Example -- 7 Iterated Product -- 7.1 Examples -- 8 Conclusion and Future Work -- A Proof that Product Equals Sequence -- References -- Sound and Complete Type Inference for Closed Effect Rows -- 1 Introduction -- 2 Motivation -- 2.1 Algebraic Effects and Handlers -- 2.2 Naive Hindley-Milner Type Inference with Algebraic Effects and Handlers -- 2.3 Type Inference with open and close -- 3 Implicitly Typed Calculus for Algebraic Effects and Handlers -- 3.1 Syntax -- 3.2 Declarative Type Inference Rules -- 4 Syntax-Directed Type Inference Rules -- 4.1 Type Substitution -- 4.2 Type Ordering -- 4.3 Inference Rules with open and close -- 4.4 Principles on the Use of [let] Rule -- 4.5 Fragility of [let] Rule -- 5 Type Inference Algorithm -- 5.1 Auxiliary Functions -- 5.2 Unification Algorithm -- 5.3 Type Inference Algorithm -- 6 Related Work -- 7 Conclusion and Future Work -- A System F + restrict -- B Type-Directed Translation to System F+restrict -- References -- Towards Efficient Adjustment of Effect Rows -- 1 Introduction -- 2 Overview -- 2.1 Effect Handlers -- 2.2 Evidence Passing Semantics and Row-Based Effect System -- 2.3 Effect Type Adjustment for Function Types -- 2.4 Motivating Open Floating -- 3 System Fpwo -- 3.1 Syntax -- 3.2 Dynamic Semantics -- 3.3 Static Semantics -- 3.4 Effect Rows and Closed Prefix Relation -- 4 Open Floating -- 4.1 Design of Algorithm -- 4.2 Organization of Definition -- 4.3 The Definition -- 4.4 Example -- 5 Evaluation -- 5.1 Ideal Case -- 5.2 Failure Case -- 6 Future Work -- 7 Related Work -- 8 Conclusion -- References -- Author Index. |
| Record Nr. | UNISA-996503466903316 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
TyDe '16 : proceedings of the 1st International Workshop on Type-Driven Development : September 18, 2016, Nara, Japan / / edited by James Chapman and Wouter Swierstra ; sponsored by ACM SIGPLAN
| TyDe '16 : proceedings of the 1st International Workshop on Type-Driven Development : September 18, 2016, Nara, Japan / / edited by James Chapman and Wouter Swierstra ; sponsored by ACM SIGPLAN |
| Pubbl/distr/stampa | New York : , : ACM, , 2016 |
| Descrizione fisica | 1 online resource (71 pages) |
| Disciplina | 005.13 |
| Soggetto topico |
Programming languages (Electronic computers)
Computer programs |
| ISBN | 1-4503-4435-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Altri titoli varianti |
Type-Driven Development 2016
Proceedings of the 1st International Workshop on Type-Driven Development ICFP '16 : ACM SIGPLAN International Conference on Functional Programming : Nara, Japan, September 18-22, 2016 International Conference on Functional Programming 2016 : Association for Computing Machinery Special Interest Group on Programming Languages International Conference on Functional Programming : Nara, Japan, September 18-22, 2016 |
| Record Nr. | UNINA-9910376436403321 |
| New York : , : ACM, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||