FUNARCH '24: "Applying Continuous Formal ..."
Applying Continuous Formal Methods to Cardano (Experience Report)
James Chapman, Arnaud Bailly, and Polina Vinogradova
(IOHK, United Kingdom; IOHK, France; IOHK, Canada)
Cardano is a Proof-of-Stake cryptocurrency with a market capitalisation in the tens of billions of USD and a daily volume of hundreds of millions of USD. In this paper we reflect on applying formal methods, functional architecture and Haskell to building Cardano. We describe our strategy, projects, lessons learned, the challenges we face, and how we propose to meet them.
@InProceedings{FUNARCH24p18,
author = {James Chapman and Arnaud Bailly and Polina Vinogradova},
title = {Applying Continuous Formal Methods to Cardano (Experience Report)},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {18--24},
doi = {10.1145/3677998.3678222},
year = {2024},
}
Publisher's Version
FUNARCH '24: "Applying Continuous Formal ..."
Applying Continuous Formal Methods to Cardano (Experience Report)
James Chapman, Arnaud Bailly, and Polina Vinogradova
(IOHK, United Kingdom; IOHK, France; IOHK, Canada)
Cardano is a Proof-of-Stake cryptocurrency with a market capitalisation in the tens of billions of USD and a daily volume of hundreds of millions of USD. In this paper we reflect on applying formal methods, functional architecture and Haskell to building Cardano. We describe our strategy, projects, lessons learned, the challenges we face, and how we propose to meet them.
@InProceedings{FUNARCH24p18,
author = {James Chapman and Arnaud Bailly and Polina Vinogradova},
title = {Applying Continuous Formal Methods to Cardano (Experience Report)},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {18--24},
doi = {10.1145/3677998.3678222},
year = {2024},
}
Publisher's Version
FUNARCH '24: "Bidirectional Data Transformations ..."
Bidirectional Data Transformations
Marcus Crestani, Markus Schlegel, and Marco Schneider
(Active Group, Germany)
Structured data is the foundation of software. Different components of a system may need the same information but may have different demands on its structure for reasons of performance, resource efficiency, technical constraints, convenience, and so on. For instance, transmitting data over a network requires a format that is suitable for serialization, while persisting data requires a format that is more suitable for storage. Thus, programmers need to translate data between several data structures and formats all the time. Authoring these translations manually is a lot of work because programmers need to implement the logic twice, once for each direction. This is redundant, tedious, and error-prone, and a case of low coherence. We show how using bidirectional data transformations that use functional optics like lenses and projections simplify the conversions. These ideas and techniques make converting data simple and straightforward and foster understanding of the relationship between data structures by explicitly describing their connections in a composable manner.
@InProceedings{FUNARCH24p31,
author = {Marcus Crestani and Markus Schlegel and Marco Schneider},
title = {Bidirectional Data Transformations},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {31--40},
doi = {10.1145/3677998.3678224},
year = {2024},
}
Publisher's Version
FUNARCH '24: "F3: A Compiler for Feature ..."
F3: A Compiler for Feature Engineering
Weixi Ma, Siyu Wang, Arnaud Venet, Junhua Gu, Subbu Subramanian, Rocky Liu, Yafei Yang, and Daniel P. Friedman
(Meta, USA; Indiana University, USA)
In machine learning (ML), feature engineering is a crucial step that converts raw data to model inputs. This process traditionally relies on data processing languages (typically SQL), but now faces new challenges due to advancements in ML. We present the design of F3, a domain-specific language (DSL) and compiler developed at Meta. F3 leverages approaches developed in functional programming and type theory to support the ML engineers of a platform that serves billions of users
@InProceedings{FUNARCH24p3,
author = {Weixi Ma and Siyu Wang and Arnaud Venet and Junhua Gu and Subbu Subramanian and Rocky Liu and Yafei Yang and Daniel P. Friedman},
title = {F3: A Compiler for Feature Engineering},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {3--9},
doi = {10.1145/3677998.3678220},
year = {2024},
}
Publisher's Version
FUNARCH '24: "F3: A Compiler for Feature ..."
F3: A Compiler for Feature Engineering
Weixi Ma, Siyu Wang, Arnaud Venet, Junhua Gu, Subbu Subramanian, Rocky Liu, Yafei Yang, and Daniel P. Friedman
(Meta, USA; Indiana University, USA)
In machine learning (ML), feature engineering is a crucial step that converts raw data to model inputs. This process traditionally relies on data processing languages (typically SQL), but now faces new challenges due to advancements in ML. We present the design of F3, a domain-specific language (DSL) and compiler developed at Meta. F3 leverages approaches developed in functional programming and type theory to support the ML engineers of a platform that serves billions of users
@InProceedings{FUNARCH24p3,
author = {Weixi Ma and Siyu Wang and Arnaud Venet and Junhua Gu and Subbu Subramanian and Rocky Liu and Yafei Yang and Daniel P. Friedman},
title = {F3: A Compiler for Feature Engineering},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {3--9},
doi = {10.1145/3677998.3678220},
year = {2024},
}
Publisher's Version
FUNARCH '24: "Continuations: What Have They ..."
Continuations: What Have They Ever Done for Us? (Experience Report)
Marc Kaufmann and Bogdan Popa
(Central European University, Austria; Independent, Romania)
Surveys and experiments in economics involve stateful interactions: participants receive different messages based on earlier answers, choices, and performance, or trade across many rounds with other participants. In the design of Congame, a platform for running such economic studies, we decided to use delimited continuations to manage the common flow of participants through a study. Here we report on the positives of this approach, as well as some challenges of using continuations, such as persisting data across requests, working with dynamic variables, avoiding memory leaks, and the difficulty of debugging continuations.
@InProceedings{FUNARCH24p25,
author = {Marc Kaufmann and Bogdan Popa},
title = {Continuations: What Have They Ever Done for Us? (Experience Report)},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {25--30},
doi = {10.1145/3677998.3678223},
year = {2024},
}
Publisher's Version
FUNARCH '24: "F3: A Compiler for Feature ..."
F3: A Compiler for Feature Engineering
Weixi Ma, Siyu Wang, Arnaud Venet, Junhua Gu, Subbu Subramanian, Rocky Liu, Yafei Yang, and Daniel P. Friedman
(Meta, USA; Indiana University, USA)
In machine learning (ML), feature engineering is a crucial step that converts raw data to model inputs. This process traditionally relies on data processing languages (typically SQL), but now faces new challenges due to advancements in ML. We present the design of F3, a domain-specific language (DSL) and compiler developed at Meta. F3 leverages approaches developed in functional programming and type theory to support the ML engineers of a platform that serves billions of users
@InProceedings{FUNARCH24p3,
author = {Weixi Ma and Siyu Wang and Arnaud Venet and Junhua Gu and Subbu Subramanian and Rocky Liu and Yafei Yang and Daniel P. Friedman},
title = {F3: A Compiler for Feature Engineering},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {3--9},
doi = {10.1145/3677998.3678220},
year = {2024},
}
Publisher's Version
FUNARCH '24: "F3: A Compiler for Feature ..."
F3: A Compiler for Feature Engineering
Weixi Ma, Siyu Wang, Arnaud Venet, Junhua Gu, Subbu Subramanian, Rocky Liu, Yafei Yang, and Daniel P. Friedman
(Meta, USA; Indiana University, USA)
In machine learning (ML), feature engineering is a crucial step that converts raw data to model inputs. This process traditionally relies on data processing languages (typically SQL), but now faces new challenges due to advancements in ML. We present the design of F3, a domain-specific language (DSL) and compiler developed at Meta. F3 leverages approaches developed in functional programming and type theory to support the ML engineers of a platform that serves billions of users
@InProceedings{FUNARCH24p3,
author = {Weixi Ma and Siyu Wang and Arnaud Venet and Junhua Gu and Subbu Subramanian and Rocky Liu and Yafei Yang and Daniel P. Friedman},
title = {F3: A Compiler for Feature Engineering},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {3--9},
doi = {10.1145/3677998.3678220},
year = {2024},
}
Publisher's Version
FUNARCH '24: "Continuations: What Have They ..."
Continuations: What Have They Ever Done for Us? (Experience Report)
Marc Kaufmann and Bogdan Popa
(Central European University, Austria; Independent, Romania)
Surveys and experiments in economics involve stateful interactions: participants receive different messages based on earlier answers, choices, and performance, or trade across many rounds with other participants. In the design of Congame, a platform for running such economic studies, we decided to use delimited continuations to manage the common flow of participants through a study. Here we report on the positives of this approach, as well as some challenges of using continuations, such as persisting data across requests, working with dynamic variables, avoiding memory leaks, and the difficulty of debugging continuations.
@InProceedings{FUNARCH24p25,
author = {Marc Kaufmann and Bogdan Popa},
title = {Continuations: What Have They Ever Done for Us? (Experience Report)},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {25--30},
doi = {10.1145/3677998.3678223},
year = {2024},
}
Publisher's Version
FUNARCH '24: "Architecting Functional Programs ..."
Architecting Functional Programs (Keynote)
Marco Sampellegrini
(Independent, Milan, Italy)
Functional programming in the small works great. Things start to get shaky when there are many services and teams involved, something that is becoming more and more common with large distributed systems.
@InProceedings{FUNARCH24p1,
author = {Marco Sampellegrini},
title = {Architecting Functional Programs (Keynote)},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {1--2},
doi = {10.1145/3677998.3678219},
year = {2024},
}
Publisher's Version
FUNARCH '24: "Bidirectional Data Transformations ..."
Bidirectional Data Transformations
Marcus Crestani, Markus Schlegel, and Marco Schneider
(Active Group, Germany)
Structured data is the foundation of software. Different components of a system may need the same information but may have different demands on its structure for reasons of performance, resource efficiency, technical constraints, convenience, and so on. For instance, transmitting data over a network requires a format that is suitable for serialization, while persisting data requires a format that is more suitable for storage. Thus, programmers need to translate data between several data structures and formats all the time. Authoring these translations manually is a lot of work because programmers need to implement the logic twice, once for each direction. This is redundant, tedious, and error-prone, and a case of low coherence. We show how using bidirectional data transformations that use functional optics like lenses and projections simplify the conversions. These ideas and techniques make converting data simple and straightforward and foster understanding of the relationship between data structures by explicitly describing their connections in a composable manner.
@InProceedings{FUNARCH24p31,
author = {Marcus Crestani and Markus Schlegel and Marco Schneider},
title = {Bidirectional Data Transformations},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {31--40},
doi = {10.1145/3677998.3678224},
year = {2024},
}
Publisher's Version
FUNARCH '24: "Bidirectional Data Transformations ..."
Bidirectional Data Transformations
Marcus Crestani, Markus Schlegel, and Marco Schneider
(Active Group, Germany)
Structured data is the foundation of software. Different components of a system may need the same information but may have different demands on its structure for reasons of performance, resource efficiency, technical constraints, convenience, and so on. For instance, transmitting data over a network requires a format that is suitable for serialization, while persisting data requires a format that is more suitable for storage. Thus, programmers need to translate data between several data structures and formats all the time. Authoring these translations manually is a lot of work because programmers need to implement the logic twice, once for each direction. This is redundant, tedious, and error-prone, and a case of low coherence. We show how using bidirectional data transformations that use functional optics like lenses and projections simplify the conversions. These ideas and techniques make converting data simple and straightforward and foster understanding of the relationship between data structures by explicitly describing their connections in a composable manner.
@InProceedings{FUNARCH24p31,
author = {Marcus Crestani and Markus Schlegel and Marco Schneider},
title = {Bidirectional Data Transformations},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {31--40},
doi = {10.1145/3677998.3678224},
year = {2024},
}
Publisher's Version
FUNARCH '24: "Design and Implementation ..."
Design and Implementation of a Verified Interpreter for Additive Manufacturing Programs (Experience Report)
Matthew Sottile and Mohit Tekriwal
(Lawrence Livermore National Laboratory, USA)
This paper describes the design of a verified tool for analyzing tool paths defined in the RS-274 language for 3D printing systems. We describe how the analyzer was designed to allow a mixture of verification and code-extraction techniques to be combined for constructing a correct toolpath analyzer written in the OCaml language. We show how we moved from a fully hand-written OCaml program to one incorporating verified components, highlighting architectural decisions that were made to facilitate this process. Finally, we share a set of architectural lessons that are generally applicable to other software with a similar goal of integration of verified components.
@InProceedings{FUNARCH24p10,
author = {Matthew Sottile and Mohit Tekriwal},
title = {Design and Implementation of a Verified Interpreter for Additive Manufacturing Programs (Experience Report)},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {10--17},
doi = {10.1145/3677998.3678221},
year = {2024},
}
Publisher's Version
FUNARCH '24: "F3: A Compiler for Feature ..."
F3: A Compiler for Feature Engineering
Weixi Ma, Siyu Wang, Arnaud Venet, Junhua Gu, Subbu Subramanian, Rocky Liu, Yafei Yang, and Daniel P. Friedman
(Meta, USA; Indiana University, USA)
In machine learning (ML), feature engineering is a crucial step that converts raw data to model inputs. This process traditionally relies on data processing languages (typically SQL), but now faces new challenges due to advancements in ML. We present the design of F3, a domain-specific language (DSL) and compiler developed at Meta. F3 leverages approaches developed in functional programming and type theory to support the ML engineers of a platform that serves billions of users
@InProceedings{FUNARCH24p3,
author = {Weixi Ma and Siyu Wang and Arnaud Venet and Junhua Gu and Subbu Subramanian and Rocky Liu and Yafei Yang and Daniel P. Friedman},
title = {F3: A Compiler for Feature Engineering},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {3--9},
doi = {10.1145/3677998.3678220},
year = {2024},
}
Publisher's Version
FUNARCH '24: "Design and Implementation ..."
Design and Implementation of a Verified Interpreter for Additive Manufacturing Programs (Experience Report)
Matthew Sottile and Mohit Tekriwal
(Lawrence Livermore National Laboratory, USA)
This paper describes the design of a verified tool for analyzing tool paths defined in the RS-274 language for 3D printing systems. We describe how the analyzer was designed to allow a mixture of verification and code-extraction techniques to be combined for constructing a correct toolpath analyzer written in the OCaml language. We show how we moved from a fully hand-written OCaml program to one incorporating verified components, highlighting architectural decisions that were made to facilitate this process. Finally, we share a set of architectural lessons that are generally applicable to other software with a similar goal of integration of verified components.
@InProceedings{FUNARCH24p10,
author = {Matthew Sottile and Mohit Tekriwal},
title = {Design and Implementation of a Verified Interpreter for Additive Manufacturing Programs (Experience Report)},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {10--17},
doi = {10.1145/3677998.3678221},
year = {2024},
}
Publisher's Version
FUNARCH '24: "F3: A Compiler for Feature ..."
F3: A Compiler for Feature Engineering
Weixi Ma, Siyu Wang, Arnaud Venet, Junhua Gu, Subbu Subramanian, Rocky Liu, Yafei Yang, and Daniel P. Friedman
(Meta, USA; Indiana University, USA)
In machine learning (ML), feature engineering is a crucial step that converts raw data to model inputs. This process traditionally relies on data processing languages (typically SQL), but now faces new challenges due to advancements in ML. We present the design of F3, a domain-specific language (DSL) and compiler developed at Meta. F3 leverages approaches developed in functional programming and type theory to support the ML engineers of a platform that serves billions of users
@InProceedings{FUNARCH24p3,
author = {Weixi Ma and Siyu Wang and Arnaud Venet and Junhua Gu and Subbu Subramanian and Rocky Liu and Yafei Yang and Daniel P. Friedman},
title = {F3: A Compiler for Feature Engineering},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {3--9},
doi = {10.1145/3677998.3678220},
year = {2024},
}
Publisher's Version
FUNARCH '24: "Applying Continuous Formal ..."
Applying Continuous Formal Methods to Cardano (Experience Report)
James Chapman, Arnaud Bailly, and Polina Vinogradova
(IOHK, United Kingdom; IOHK, France; IOHK, Canada)
Cardano is a Proof-of-Stake cryptocurrency with a market capitalisation in the tens of billions of USD and a daily volume of hundreds of millions of USD. In this paper we reflect on applying formal methods, functional architecture and Haskell to building Cardano. We describe our strategy, projects, lessons learned, the challenges we face, and how we propose to meet them.
@InProceedings{FUNARCH24p18,
author = {James Chapman and Arnaud Bailly and Polina Vinogradova},
title = {Applying Continuous Formal Methods to Cardano (Experience Report)},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {18--24},
doi = {10.1145/3677998.3678222},
year = {2024},
}
Publisher's Version
FUNARCH '24: "F3: A Compiler for Feature ..."
F3: A Compiler for Feature Engineering
Weixi Ma, Siyu Wang, Arnaud Venet, Junhua Gu, Subbu Subramanian, Rocky Liu, Yafei Yang, and Daniel P. Friedman
(Meta, USA; Indiana University, USA)
In machine learning (ML), feature engineering is a crucial step that converts raw data to model inputs. This process traditionally relies on data processing languages (typically SQL), but now faces new challenges due to advancements in ML. We present the design of F3, a domain-specific language (DSL) and compiler developed at Meta. F3 leverages approaches developed in functional programming and type theory to support the ML engineers of a platform that serves billions of users
@InProceedings{FUNARCH24p3,
author = {Weixi Ma and Siyu Wang and Arnaud Venet and Junhua Gu and Subbu Subramanian and Rocky Liu and Yafei Yang and Daniel P. Friedman},
title = {F3: A Compiler for Feature Engineering},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {3--9},
doi = {10.1145/3677998.3678220},
year = {2024},
}
Publisher's Version
FUNARCH '24: "F3: A Compiler for Feature ..."
F3: A Compiler for Feature Engineering
Weixi Ma, Siyu Wang, Arnaud Venet, Junhua Gu, Subbu Subramanian, Rocky Liu, Yafei Yang, and Daniel P. Friedman
(Meta, USA; Indiana University, USA)
In machine learning (ML), feature engineering is a crucial step that converts raw data to model inputs. This process traditionally relies on data processing languages (typically SQL), but now faces new challenges due to advancements in ML. We present the design of F3, a domain-specific language (DSL) and compiler developed at Meta. F3 leverages approaches developed in functional programming and type theory to support the ML engineers of a platform that serves billions of users
@InProceedings{FUNARCH24p3,
author = {Weixi Ma and Siyu Wang and Arnaud Venet and Junhua Gu and Subbu Subramanian and Rocky Liu and Yafei Yang and Daniel P. Friedman},
title = {F3: A Compiler for Feature Engineering},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {3--9},
doi = {10.1145/3677998.3678220},
year = {2024},
}
Publisher's Version