folks working in theoretical PL or logic/math-adjacent CS: if someone in your department were teaching a "research methods" class and wanted you to suggest some readings related to the methods used in your field, what would you send them?
i've had lots of interesting conversations about this, but what's been written and published? (i'm also interested in your opinions even if they're not written down in papers, but secondarily.)
Sep 11, 2026, 7:27 PM@chrisamaphone A draft that I had helped read but never got published was this on mechanizing a logical relation for dependent types to prove consistency https://electriclam.com/papers/mltt.pdf by Yiyun Liu
Our other joint papers as well as one of my own (unpublished) extends this basic technique to our respective dependent type theories
I would add to this the POPLMark reloaded paper https://doi.org/10.1017/S0956796819000170 but specifically the part about the inductive characterization of SN in section 3.2, which Yiyun had used in combination with the above in a later paper, and which I used to mechanize strong normalization of CBPV (just as an exercise)
This inductive characterization just makes more sense to me in my brain than than how I was originally taught this stuff, using Girard's candidats de réducibilité, and it was much easier to grasp how I needed to extend it for CBPV
If I needed to mechanize strong normalization of anything wrt a small step semantics via logical relations this combo is what I would refer to, even if it's not dependent — it always seems easier to me to simplify from dependent types than to extend from simple types
As for normalization wrt big step semantics via logical relations luckily Emma Suárez had written about this as a proof pearl back when he was at PLClub https://arxiv.org/abs/2309.15724 unfortunately it also did not get published. It's pretty annoying that writing down proof techniques that """aren't novel""" doesn't get you publications
@chrisamaphone I'm not sure there is much of a method to this besides "stare at problem, think hard, write down solution?"
Perhaps "stare at problem, type solution into the computer (ITP), the computer complains, iterate until it stops complaining, admire actual solution?"
There are various techniques for how to best attack certain problems and a rather large part of this is knowing which techniques work for which problems.
@chrisamaphone This is not a recommendation from me, since I've never read it (though I mean to), but I have had it recommended to me probably several times (including by Derek Dreyer I think): Imre Lakatos's Proofs and Refutations: The Logic of Mathematical Discovery
@rg9119 @chrisamaphone I’ll second that rec! proofs and refutations is great. I had not thought of it in the context of CS, but the iterative development ideas in it would probably be really interesting for cs research.
@rg9119 people also keep recommending Proofs and Refutations to me, and i also, lamentably, have not yet read it. maybe we should start a reading group...
@chrisamaphone @rg9119 I, too, have an unread copy of that one 😢
@chrisamaphone @rg9119 I read part of it a couple months ago! I liked it a lot so far.
I also found it easier to read than the title sorta suggests... I should finish it sometime. Haven't seen too many other math books that are entirely in the form of a dialogue (other than Surreal Numbers by Knuth).
@roboguy There are some, like Heyting's Intuitionism, but I've always found they get annoying fast
Sep 12, 2026, 12:21 PM@rg9119 @chrisamaphone Alison Pease wrote a thesis on "A Computational Model of Lakatos-style Reasoning" as a way of formalising how theories are built. https://era.ed.ac.uk/server/api/core/bitstreams/4fea9809-7570-4d56-a033-5204393e1a6a/content
There's various follow up papers, slide decks and videoed talks she's done as well, including surveys of how real mathematicians work with Ursula Martin
@chrisamaphone First thing which comes to mind, although I've never read it first hand (but one of my undergrand math prof drilled many of its concepts into us): Polya's How to Solve It. I've also recently become a big evangelist for Naur's Programming as Theory Building, although whether this counts as research and methodology is probably debatable
Sep 12, 2026, 7:48 AMI still maintain I am not core PL/Maths trained, but the following, I think, helps:
I’m going to suggest @edwinb TDD book. Not because it is about Idris, but helps getting you to think about the problem before attempting the solution.
Not to mention: https://www.sigplan.org/Resources/EmpiricalEvaluation/ because mechanisation means we are more ‘wet’ in our science than before…
I’m partial to: How to write and publish a scientific paper by Day & Gastal. Because communicating our research helps with how best to do it.
Not to mention anything on research journalling and lab diaries. We are supposed to be a science, many of us do not science!
Sep 12, 2026, 9:20 AM@chrisamaphone I like the book "Mechanizing Proof" by Donald MacKenzie. It is a sociological history of doing maths with and about computers.
Sep 12, 2026, 9:40 AM@chrisamaphone More directly on Research Methods is "The researchers' bible" by Alan Bundy, Ben du Boulay, Jim Howe, and Gordon Plotkin, 1985. https://www.pure.ed.ac.uk/ws/portalfiles/portal/15537012/researchers_bible_95.pdf
@bentnib this one came up in the literature search we did for the Futureproof paper! i think i tried to get a digital copy at some point...
@chrisamaphone @bentnib i have a hard copy at BC if you want to borrow it
Sep 12, 2026, 11:33 AM@chrisamaphone I suggest Mark Priestley. The Algol Research Programme. https://link.springer.com/chapter/10.1007/978-1-84882-555-0_9
@gadmm oooh i really like this suggestion