Kamal Aboul-Hosn

Email: kamal at cs.cornell.edu

I work on Pub/Sub at Google. I also play drums for The Purslaines. I completed my Ph.D. at Cornell University in Department of Computer Science in 2007. I worked in the areas of automated reasoning, theorem provers, and program verification with Dexter Kozen. All of these exciting things are summed up in my LinkedIn page.

Photo by the great Alan Rand.

Email: kamal at cs.cornell.edu

I work on Pub/Sub at Google. I also play drums for The Purslaines. I completed my Ph.D. at Cornell University in Department of Computer Science in 2007. I worked in the areas of automated reasoning, theorem provers, and program verification with Dexter Kozen. All of these exciting things are summed up in my LinkedIn page.

Photo by the great Alan Rand.

Publications | Kamal Aboul-Hosn. A Proof-Theoretic Approach to Mathematical Knowledge Management. Ph.D. Dissertation, Cornell University, January 2007. |

Kamal Aboul-Hosn. An Axiomatization of Arrays for Kleene Algebra with Tests. In R. A. Schmidt, editor, Proc. 9th Int. Conf. Relational Methods in Computer Science and 4th Int. Workshop Applications of Kleene Algebra (RelMiCS/AKA'06), volume 4136 of Lecture Notes in Computer Science, pages 63-77. Springer, August 2006. (Tech report version with more complete proofs) | |

Kamal Aboul-Hosn and Dexter Kozen. Local variable scoping and Kleene algebra with tests. In R. A. Schmidt, editor, Proc. 9th Int. Conf. Relational Methods in Computer Science and 4th Int. Workshop Applications of Kleene Algebra (RelMiCS/AKA'06), volume 4136 of Lecture Notes in Computer Science, pages 78-90. Springer, August 2006. | |

Kamal Aboul-Hosn. A Proof-Theoretic Approach to Tactics. In Borwein, Jonathan M.; Farmer, William M., editors, Proc. 5th Int. Conf. Mathematical Knowledge Management (MKM'06), volume 4108 of Lecture Notes in Computer Science, pages 54-66. Springer, August 2006. | |

Kamal Aboul-Hosn and Dexter Kozen. Relational semantics for higher-order programs. In Tarmo Uustalu, editor, Proc. 8th Int. Conf. Mathematics of Program Construction (MPC'06), volume 4014 of Lecture Notes in Computer Science, pages 29-48. Springer, July 2006. | |

Kamal Aboul-Hosn and Dexter Kozen. KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests. Journal of Applied non-Classical Logics, 2006(1). 2006. | |

Kamal Aboul-Hosn and Dexter Kozen. Relational Semantics of Local Variable Scoping. Technical Report 2005-2000, Computer Science Department, Cornell University, July 2005. | |

Kamal Aboul-Hosn and Terese Damhøj Andersen. A Proof-Theoretic Approach to Hierarchical Math Library Organization. In Proc. 4th Int. Mathematical Knowledge Management Conference, pages 1-16. International University of Bremen, October 2005. | |

Kamal Aboul-Hosn and Dexter Kozen. KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests. In Proc. 4th Int. Workshop on the Implementation of Logics, pages 2-12. University of Manchester, September 2003. | |

Kamal Aboul-Hosn. Programming with Private State. Honors Thesis, The Pennsylvania State University, December 2001. | |

Presentations | Local Variable Scoping and Kleene Algebra with Tests. RelMiCS 06, Manchester, UK. |

An Axiomatization of Arrays for Kleene Algebra with Tests. RelMiCS 06, Manchester, UK. | |

A Proof-Theoretic Approach to Tactics. MKM 06, Wokingham, UK. | |

Relational Semantics for Higher-Order Programs. MPC 06, Kuressaare, Estonia. | |

Relational Semantics of Local Variable Scoping.PLDG Fall 2005, Cornell University. | |

A Proof-Theoretic Approach to Hierarchical Math Library Organization. MKM 05, Bremen, Germany. | |

KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests. PLDG Spring 2004, Cornell University. | |

KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests. WIL 03, Almaty, Kazakhstan. | |

Courses TAed | CS 100J: Introduction to Computer Programming |

CS 472/473: Foundations of Artificial Intelligence | |

CS 130: Introduction to Web Documents | |

CS 312: Data Structures and Functional Programming | |

CS 481: Automata and Computability | |

Projects | KAT-ML - An interactive theorem prover for Kleene algebra with tests |

Can Computers Think? - GSSOP high school mini-course | |

Radar In Motion - Mac OS X Dashboard widget | |

Lambda Prolog Projects - Parser Generator, Emacs Module, and String Library for the Lambda Prolog Language |