Lawrence Charles Paulson (born 1955) is a professor at the University of Cambridge Computer Laboratory and a fellow of Clare College. He is best known for the cornerstone text on the programming language ML, ML for the Working Programmer . His research is based around the interactive theorem prover Isabelle. He has worked on the verification of cryptographic protocols using inductive definitions, and he has also formalized the constructible universe of Kurt Gödel.

PropertyValue
dbpedia-owl:Person/almaMater
dbpedia-owl:Person/birthDate
  • 1955-01-01 00:00:00 (xsd:date)
dbpedia-owl:Person/knownFor
dbpedia-owl:almaMater
dbpedia-owl:birthDate
  • 1955-01-01 00:00:00 (xsd:date)
dbpedia-owl:knownFor
dbpprop:abstract
  • Lawrence Charles Paulson (born 1955) is a professor at the University of Cambridge Computer Laboratory and a fellow of Clare College. He is best known for the cornerstone text on the programming language ML, ML for the Working Programmer . His research is based around the interactive theorem prover Isabelle. He has worked on the verification of cryptographic protocols using inductive definitions, and he has also formalized the constructible universe of Kurt Gödel. Current research projects are described on his web page. Paulson graduated from the California Institute of Technology in 1977, and obtained his PhD in Computer Science from Stanford University. He came to the University of Cambridge in 1983 and became a fellow in 1987. He is married, with two children. He is a Fellow of the Association for Computing Machinery (2008).
dbpprop:almaMater
dbpprop:dateOfBirth
  • 1955 (xsd:integer)
dbpprop:hasPhotoCollection
dbpprop:knownFor
dbpprop:name
  • Lawrence Paulson
dbpprop:reference
dbpprop:wikiPageUsesTemplate
dbpprop:workplaces
rdf:type
rdfs:comment
  • Lawrence Charles Paulson (born 1955) is a professor at the University of Cambridge Computer Laboratory and a fellow of Clare College. He is best known for the cornerstone text on the programming language ML, ML for the Working Programmer . His research is based around the interactive theorem prover Isabelle. He has worked on the verification of cryptographic protocols using inductive definitions, and he has also formalized the constructible universe of Kurt Gödel.
rdfs:label
  • Lawrence Paulson
owl:sameAs
skos:subject
foaf:name
  • Lawrence Paulson
foaf:page
is dbpprop:redirect of
is owl:sameAs of