People (tentative):

• Ruzica
• Philippe
• Jiewen
• Damien

• Isabelle-based surface syntax
• HOTPTP
• SMT-LIB

• SUGA axiomatization from my paper with D.Jackson
• Fagin's theorem, its consequences on spec language design on finite models, finite domain complexity in practice
• Ahrendt's work
• completion for finding infinite models, presentation of infinite models
• using Ehrenfeucht-Feferman games to find models

References:

• Geometric resolution: A Proof Procedure based on Finite Model Search
• Darwin
• Wolfgang Reif

• integer linear arithmetic
• interpolant combination
• interpolants for modal mu calculus and MSOL

• programs as formulas, formulas as proofs
• tactic style proofs
• Scala as computational logic

General theme: give more than yes/no answers.