Publications

Filtered as: all types - all years - author: Zaliva, Vadim - all keywords
Sorted by: keyword
Corresponding bibtex list 

Coding/Decoding 

1. Vadim Zaliva
   HELIX: From Math to Verified Code
   PhD. thesis, Electrical and Computer Engineering, Carnegie Mellon University, 2020
   

Coq 

1. Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva and Steve Zdancewic
   Modular, Compositional, and Executable Formal Semantics for LLVMIR
   Proc. International Conference on Functional Programming (ICFP), 2021
   
2. Vadim Zaliva, Ilia Zaichuk and Franz Franchetti
   Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX
   Proc. Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2020
   
3. Vadim Zaliva and Matthieu Sozeau
   Reification of Shallow-Embedded DSLs in Coq with Automated Verification
   Proc. International Workshop on Coq for Programming Languages (CoqPL), 2019
   

Domain-specific 

1. Vadim Zaliva, Ilia Zaichuk and Franz Franchetti
   Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX
   Proc. Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2020
   

Embedded DSLs 

1. Vadim Zaliva and Matthieu Sozeau
   Reification of Shallow-Embedded DSLs in Coq with Automated Verification
   Proc. International Workshop on Coq for Programming Languages (CoqPL), 2019
   

HELIX 

1. Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva and Steve Zdancewic
   Modular, Compositional, and Executable Formal Semantics for LLVMIR
   Proc. International Conference on Functional Programming (ICFP), 2021
   
2. Vadim Zaliva
   HELIX: From Math to Verified Code
   PhD. thesis, Electrical and Computer Engineering, Carnegie Mellon University, 2020
   
3. Vadim Zaliva, Ilia Zaichuk and Franz Franchetti
   Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX
   Proc. Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2020
   

High performance 

1. Vadim Zaliva and Franz Franchetti
   HELIX: A Case Study of a Formal Verification of High Performance Program Generation
   Proc. Workshop on Functional High Performance Computing (FHPC), 2018
   

LLVM 

1. Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva and Steve Zdancewic
   Modular, Compositional, and Executable Formal Semantics for LLVMIR
   Proc. International Conference on Functional Programming (ICFP), 2021
   

Monads 

1. Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva and Steve Zdancewic
   Modular, Compositional, and Executable Formal Semantics for LLVMIR
   Proc. International Conference on Functional Programming (ICFP), 2021
   

Program generation 

1. Vadim Zaliva and Franz Franchetti
   HELIX: A Case Study of a Formal Verification of High Performance Program Generation
   Proc. Workshop on Functional High Performance Computing (FHPC), 2018
   

Semantics 

1. Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva and Steve Zdancewic
   Modular, Compositional, and Executable Formal Semantics for LLVMIR
   Proc. International Conference on Functional Programming (ICFP), 2021
   

Verification 

1. Vadim Zaliva
   HELIX: From Math to Verified Code
   PhD. thesis, Electrical and Computer Engineering, Carnegie Mellon University, 2020
   
2. Vadim Zaliva, Ilia Zaichuk and Franz Franchetti
   Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX
   Proc. Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2020
   
3. Vadim Zaliva and Matthieu Sozeau
   Reification of Shallow-Embedded DSLs in Coq with Automated Verification
   Proc. International Workshop on Coq for Programming Languages (CoqPL), 2019
   

Verified compilation 

1. Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva and Steve Zdancewic
   Modular, Compositional, and Executable Formal Semantics for LLVMIR
   Proc. International Conference on Functional Programming (ICFP), 2021
   

(No keyword) 

1. Vadim Zaliva and Franz Franchetti
   Barometric and GPS Altitude Sensor Fusion
   Proc. International Conference on Acoustics, Speech, and Signal Processing (ICASSP), 2014
   

Publication interface designed and implemented by Patra Pantupat, Aliaksei Sandryhaila, and Markus Püschel
Electrical and Computer Engineering, Carnegie Mellon University, 2007