Amin Timany

According to our database1, Amin Timany authored at least 21 papers between 2015 and 2021.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2021
Fully abstract from static to gradual.
Proc. ACM Program. Lang., 2021

Mechanized logical relations for termination-insensitive noninterference.
Proc. ACM Program. Lang., 2021

Distributed causal memory: modular specification and verification in higher-order distributed separation logic.
Proc. ACM Program. Lang., 2021

Efficient and provable local capability revocation using uninitialized capabilities.
Proc. ACM Program. Lang., 2021

Reasoning about monotonicity in separation logic.
Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020
The future is ours: prophecy variables in separation logic.
Proc. ACM Program. Lang., 2020

Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris.
Proc. ACM Program. Lang., 2020

Leibniz equality is isomorphic to Martin-Löf identity, parametrically.
J. Funct. Program., 2020

A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit.
CoRR, 2020

A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report.
CoRR, 2020

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems.
Proceedings of the Programming Languages and Systems, 2020

2019
Mechanized relational verification of concurrent programs with continuations.
Proc. ACM Program. Lang., 2019

Abstract I/O Specification.
CoRR, 2019

Specifying I/O using abstract nested hoare triples in separation logic.
Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, 2019

2018
A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST.
Proc. ACM Program. Lang., 2018

MoSeL: a general, extensible modal framework for interactive proofs in separation logic.
Proc. ACM Program. Lang., 2018

Cumulative Inductive Types In Coq.
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

2017
Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC).
CoRR, 2017

Interactive proofs in higher-order concurrent separation logic.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016
Category Theory in Coq 8.5.
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

2015
First Steps Towards Cumulative Inductive Types in CIC.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2015, 2015


  Loading...