Follow
Amin Timany
Title
Cited by
Cited by
Year
Interactive proofs in higher-order concurrent separation logic
R Krebbers, A Timany, L Birkedal
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming …, 2017
2042017
MoSeL: A general, extensible modal framework for interactive proofs in separation logic
R Krebbers, JH Jourdan, R Jung, J Tassarotti, JO Kaiser, A Timany, ...
Proceedings of the ACM on Programming Languages 2 (ICFP), 1-30, 2018
1092018
The future is ours: prophecy variables in separation logic
R Jung, R Lepigre, G Parthasarathy, M Rapoport, A Timany, D Dreyer, ...
Proceedings of the ACM on Programming Languages 4 (POPL), 1-32, 2019
752019
A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of runST
A Timany, L Stefanesco, M Krogh-Jespersen, L Birkedal
Proceedings of the ACM on Programming Languages 2 (POPL), 1-28, 2017
682017
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
M Krogh-Jespersen, A Timany, ME Ohlenbusch, SO Gregersen, ...
European Symposium on Programming, 336-365, 2020
512020
Efficient and provable local capability revocation using uninitialized capabilities
AL Georges, A Guéneau, T Van Strydonck, A Timany, A Trieu, ...
Proceedings of the ACM on Programming Languages 5 (POPL), 1-30, 2021
362021
Mechanized relational verification of concurrent programs with continuations
A Timany, L Birkedal
Proceedings of the ACM on Programming Languages 3 (ICFP), 1-28, 2019
342019
Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris
PG Giarrusso, L Stefanesco, A Timany, L Birkedal, R Krebbers
Proceedings of the ACM on Programming Languages 4 (ICFP), 1-29, 2020
242020
Distributed causal memory: modular specification and verification in higher-order distributed separation logic
L Gondelman, SO Gregersen, A Nieto, A Timany, L Birkedal
Proceedings of the ACM on Programming Languages 5 (POPL), 1-29, 2021
222021
Consistency of the predicative calculus of cumulative inductive constructions (pCuIC)
A Timany, M Sozeau
arXiv preprint arXiv:1710.03912, 2017
222017
A logical approach to type soundness
A Timany, R Krebbers, D Dreyer, L Birkedal
Journal of the ACM 71 (6), 1-75, 2024
212024
Trillium: higher-order concurrent and distributed separation logic for intensional refinement
A Timany, SO Gregersen, L Stefanesco, JK Hinrichsen, L Gondelman, ...
Proceedings of the ACM on Programming Languages 8 (POPL), 241-272, 2024
20*2024
Category Theory in Coq 8.5
A Timany, B Jacobs
1st International Conference on Formal Structures for Computation and …, 2016
202016
Fully abstract from static to gradual
K Jacobs, A Timany, D Devriese
Proceedings of the ACM on Programming Languages 5 (POPL), 1-30, 2021
192021
Mechanized logical relations for termination-insensitive noninterference
SO Gregersen, J Bay, A Timany, L Birkedal
Proceedings of the ACM on Programming Languages 5 (POPL), 1-29, 2021
182021
Cumulative inductive types in Coq
A Timany, M Sozeau
3rd International Conference on Formal Structures for Computation and …, 2018
182018
Reasoning about monotonicity in separation logic
A Timany, L Birkedal
Proceedings of the 10th ACM SIGPLAN International Conference on Certified …, 2021
162021
Verifying reliable network components in a distributed separation logic with dependent separation protocols
L Gondelman, JK Hinrichsen, M Pereira, A Timany, L Birkedal
Proceedings of the ACM on Programming Languages 7 (ICFP), 847-877, 2023
152023
Modular verification of op-based CRDTs in separation logic
A Nieto, L Gondelman, A Reynaud, A Timany, L Birkedal
Proceedings of the ACM on Programming Languages 6 (OOPSLA2), 1788-1816, 2022
152022
First steps towards cumulative inductive types in CIC
A Timany, B Jacobs
Theoretical Aspects of Computing-ICTAC 2015: 12th International Colloquium …, 2015
132015
The system can't perform the operation now. Try again later.
Articles 1–20