Travelled to:1 × USA
Collaborated with:M.O.Myreen M.Norrish Y.K.Tan S.Owens Y.Nagashima O.Abrahamsson A.Guéneau S.Ho Andreas Lööw Anthony C. J. Fox
Talks about:verifi (4) ml (4) proof (3) cake (3) function (2) hol (2) characterist (1) processor (1) implement (1) synthesi (1)
Person: Ramana Kumar
DBLP: Kumar:Ramana
Contributed to:
2014
20162017
2017
2018
2019Wrote 6 papers:
- POPL-2014-KumarMNO #implementation #ml #named
- CakeML: a verified implementation of ML (RK, MOM, MN, SO), pp. 179–192.
- ESOP-2016-OwensMKT #functional #semantics
- Functional Big-Step Semantics (SO, MOM, RK, YKT), pp. 589–615.
- ESOP-2017-GueneauMKN
- Verified Characteristic Formulae for CakeML (AG, MOM, RK, MN), pp. 584–610.
- CADE-2017-NagashimaK #generative #higher-order #proving
- A Proof Strategy Language and Proof Script Generation for Isabelle/HOL (YN, RK), pp. 528–545.
- IJCAR-2018-HoAKMTN #monad #synthesis
- Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (SH, OA, RK, MOM, YKT, MN), pp. 646–662.
- PLDI-2019-LoowKTMNAF #compilation
- Verified compilation on a verified processor (AL, RK, YKT, MOM, MN, OA, ACJF), pp. 1041–1053.