Fall Research Expo 2021
The Formalization of Permutation Networks
Permutation networks are circuits of configurable switches, such that their output is always a permutation of the input. They were originally developed for telecommunications and later found applications in cryptography. Permutation networks have unique properties:
- Configurable → n configuration bits, n! Permutations
- Reversible → Involution
- Scalable → Poly-logarithmic number of configurations
- Parametric polymorphic → Generalization of types
- The number of inputs = the number of outputs → Must be a power of 2
In order to prove and work with permutation networks, we used a proof based programming language called Coq. We used Coq to prove and work with specific features relevant to our research.
PRESENTED BY
PURM - Penn Undergraduate Research Mentoring Program
Engineering & Applied Sciences 2024
Advised By
Stephanie Weirich
ENIAC President's Distinguished Professor of Computer and Information Science
Steve Zdancewic
Schlein Family President's Distinguished Professor and Associate Chair
PRESENTED BY
PURM - Penn Undergraduate Research Mentoring Program
Engineering & Applied Sciences 2024
Advised By
Stephanie Weirich
ENIAC President's Distinguished Professor of Computer and Information Science
Steve Zdancewic
Schlein Family President's Distinguished Professor and Associate Chair
Comments
Loved hearing about Christa's interesting research!
Christa’s choice of permutation network was the benes network! She worked with circuits and explained how this can be used in multiple ways by utilizing independent types.
Loved hearing about Christa's interesting research!
Christa’s choice of permutation network was the benes network! She worked with circuits and explained how this can be used in multiple ways by utilizing independent types.
PURM Poster meeting!
Christa used a Benes Network to describe all the properties of a permutation network. She went over how to traverse through the network and what each part meant.