Hasan Amjad

CURRENT ADDRESS
University of Cambridge Computer Laboratory
15 JJ Thomson Avenue
Cambridge CB3 0FD
United Kingdom
Tel.: +44 (01223) 763602
e-mail : ha227 at cam dot ac dot uk

DATE OF BIRTH 25th January, 1975

NATIONALITY British & Pakistani

EMPLOYMENT

Nov. 2008 to date Analyst, Cantab Capital Partners LLP, Cambridge, UK

Aug. 2007 to date Visiting Fellow, Computer Laboratory, University of Cambridge, UK

Aug. 2007 to Nov 2008 Research Associate, School of Computing, Middlesex University, UK

Oct. 2003 to Jul. 2007 Research Assistant/Associate, Computer Laboratory, University of Cambridge, UK

June 2001 to Aug. 2001 Summer Intern, Compaq Cambridge Research Labs, USA

Nov.1999 to Aug. 2000 3D Graphics Developer, Align Technology Inc., Pakistan

ADMINISTRATIVE

2008 PC member, Theorem Proving in Higher Order Logics (TPHOLs)

2007- Member, SMT-LIB working group on proof format standardisation

EDUCATION

Oct. 2000 to Sep. 2004 Ph.D. Computer Science

Automated Reasoning Group, Computer Laboratory, University of Cambridge, UK

Oct. 1998 to Oct. 1999 M.Sc. Mathematics and the Foundations of Computer Science

Mathematical Institute, University of Oxford, UK

Aug. 1994 to May 1997 B.Sc. (Hons.) Computer Science

Dept. of Computer Science, Lahore University of Management Sciences, Pakistan

AWARDS

2003 Trinity College (Cambridge) Graduate Studentship

2000 Trinity College (Cambridge) External Research Studentship (3 years)

Overseas Research Scholar Award (3 years)

Commonwealth Scholarship (Honorary)

Commonwealth Fellow

Merton College (Oxford) Harmsworth-Domus Graduate Scholarship (Declined)

1999 Worcester College (Oxford) Cash Prize for Academic Performance

Distinction in M.Sc. MFOCS programme (Oxford University, top candidate)

1996 Dean's Honours List

RESEARCH

Oct. 2004 to date Integration of SAT/SMT solvers and interactive theorem provers; propositional proof compression; analysis of concurrent heap-manipulating programs.

Oct. 2000 to Sep. 2004 For Ph.D., developed a self-verifying model checker in the HOL theorem prover. This work was supervised by Professor M. J. C. Gordon FRS.

Oct. 1998 to Sept. 1999 For M.Sc., constructed a categorical model of classical linear logic using Hoare's CSP. This work was supervised by Dr. C-H. L. Ong.

TEACHING

Oct. 2004 to date Research Assistant/Associate

Computer Laboratory, University of Cambridge, UK

In addition to supervisions, acted as moderator for second-year Discrete Maths problem solving seminars ( 15 students per session).

Taught Theory and Semantics Mini-Course titled Formal Verification Techniques.

Oct. 2000 to Sep. 2004 Research Student

Computer Laboratory, University of Cambridge, UK

Conducted undergraduate supervisions for the following courses: Concurrency, Natural Language Processing, Denotational Semantics, Theory of Computation and Quantum Computing.

July 1997 to July 1998 Teaching Assistant in Computer Science

Lahore University of Management Sciences, Pakistan

Conducted undergraduate tutorials for the following courses: Calculus, Statistics, Probability, Operations Research, Automata, Complexity Theory and Compilers (50-100 students per tutorial). Also helped set and mark exams for these courses.

Hasan 2008-11-06

Nov. 2008 to date	Analyst, Cantab Capital Partners LLP, Cambridge, UK
Aug. 2007 to date	Visiting Fellow, Computer Laboratory, University of Cambridge, UK
Aug. 2007 to Nov 2008	Research Associate, School of Computing, Middlesex University, UK
Oct. 2003 to Jul. 2007	Research Assistant/Associate, Computer Laboratory, University of Cambridge, UK
June 2001 to Aug. 2001	Summer Intern, Compaq Cambridge Research Labs, USA
Nov.1999 to Aug. 2000	3D Graphics Developer, Align Technology Inc., Pakistan

2008	PC member, Theorem Proving in Higher Order Logics (TPHOLs)
2007-	Member, SMT-LIB working group on proof format standardisation

Oct. 2000 to Sep. 2004	Ph.D. Computer Science
	Automated Reasoning Group, Computer Laboratory, University of Cambridge, UK
Oct. 1998 to Oct. 1999	M.Sc. Mathematics and the Foundations of Computer Science
	Mathematical Institute, University of Oxford, UK
Aug. 1994 to May 1997	B.Sc. (Hons.) Computer Science
	Dept. of Computer Science, Lahore University of Management Sciences, Pakistan

2003	Trinity College (Cambridge) Graduate Studentship
2000	Trinity College (Cambridge) External Research Studentship (3 years)
	Overseas Research Scholar Award (3 years)
	Commonwealth Scholarship (Honorary)
	Commonwealth Fellow
	Merton College (Oxford) Harmsworth-Domus Graduate Scholarship (Declined)
1999	Worcester College (Oxford) Cash Prize for Academic Performance
	Distinction in M.Sc. MFOCS programme (Oxford University, top candidate)
1996	Dean's Honours List

Oct. 2004 to date	Integration of SAT/SMT solvers and interactive theorem provers; propositional proof compression; analysis of concurrent heap-manipulating programs.
Oct. 2000 to Sep. 2004	For Ph.D., developed a self-verifying model checker in the HOL theorem prover. This work was supervised by Professor M. J. C. Gordon FRS.
Oct. 1998 to Sept. 1999	For M.Sc., constructed a categorical model of classical linear logic using Hoare's CSP. This work was supervised by Dr. C-H. L. Ong.

Oct. 2004 to date	Research Assistant/Associate
	Computer Laboratory, University of Cambridge, UK
	In addition to supervisions, acted as moderator for second-year Discrete Maths problem solving seminars ( 15 students per session).
	Taught Theory and Semantics Mini-Course titled Formal Verification Techniques.
Oct. 2000 to Sep. 2004	Research Student
	Computer Laboratory, University of Cambridge, UK
	Conducted undergraduate supervisions for the following courses: Concurrency, Natural Language Processing, Denotational Semantics, Theory of Computation and Quantum Computing.
July 1997 to July 1998	Teaching Assistant in Computer Science
	Lahore University of Management Sciences, Pakistan
	Conducted undergraduate tutorials for the following courses: Calculus, Statistics, Probability, Operations Research, Automata, Complexity Theory and Compilers (50-100 students per tutorial). Also helped set and mark exams for these courses.