A day to celebrate David Pym's life work

Research in the PPLV group spans logic, semantics, quantum information and computation, and verification. We study, and employ methods from, aspects of proof theory, model theory, type theory, computation theory, complexity theory, game theory, and category theory. 

In logic, interests and expertise including 

• the foundations of logic and proof theory, including proof-theoretic semantics, 
• substructural logic, including both bunched logic and linear logic, 
• reductive logic, proof-search, and logic programming,   
• algebraic logic and algebras of relations, 
• temporal and modal logics,  
• game theory,  
• categorical logic, and  
• applications of logic in security.

In semantics, we have interests and expertise that includes   

• semantics of natural language, categorial grammars, and vector space semantics,
• compositional distributional semantics,   
• Frobenius algebras and substructural modalities,  
• information flow, 
• algebraic and co-algebraic semantics of computation,
• semantics of logic programming and proof-search,
• automata and language theory,
• string diagrams, and  
• systems modelling, using ideas from process theory and logic, with applications in areas such as systems security, security policy, and surge capacity in healthcare systems.  

In quantum information and computation, we have interests and expertise including  

• high-level methods for quantum computation and information,
• categorical quantum mechanics, 
• connections between quantum information and natural language   semantics, and  
• sheaf-theoretic approaches to non-locality and contextualize. 

In verification, we have interests and expertise that includes 

• Separation Logic, Concurrent Separation Logic, and their derivatives, 
• tools --- such as Infer, Space Invader, SLAM, Terminator ---  for program analysis and verification, 
• cyclic proofs,  
• automated reasoning and machine-checked proof, 
• weak memory models, 
• cryptocurrencies, and   
• verification of program and network security properties. 

We have excellent connections with cutting-edge industry and strong connections with other groups within UCL, including the Department of Philosophy, around London, and around the world.