Practical Programming with Higher-Order Encodings and Dependent Types
No abstract available.
Related papers
- Encoding Types in ML-Like Languages ICFP 1998
- Embedding a full linear Lambda calculus in Haskell Haskell 2015
- Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System ICFP 2024
- Polymorphism and separation in hoare type theory ICFP 2006
- Static interpretation of higher-order modules in Futhark: functional GPU programming in the large ICFP 2018
- Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages JFP 2009
- Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy OOPSLA 2019
- PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs PLDI 2025