In this episode I talk with David Christiansen. We talk his introduction to functional programming, research in dependent types, Idris, Nuprl and LFC traits, work to add dependent types to macro-expansion in Racket, and much, much more.Our Guest, David Christiansen@d_christiansen on Twitterhttp://davidchristiansen.dk/Conference AnnouncementsRacketCon is October 7th & 8th at the University of Washington, with keynote speakers Dan Friedman and Will Byrd. Visit http://con.racket-lang.org/ for more information and to register.Celebrate the 10th anniversary of the release of Clojure October the 12th – 14th at the Clojure/Conj in Baltimore, Maryland. Visit http://2017.clojure-conj.org/ for more information and to register.LambdaWorld will be taking place in Cadiz, Spain on October 26th and 27th. For more information visit and to keep updated visit http://www.lambda.world/.CodeMesh is coming up November 8th and 9th in London. For more information, and to keep an eye open for registration, visit http://www.codemesh.io/.Moonconf will be taking place the 9th-11th of November. For more information visit http://moonconf.org/.Clojure SYNC will be taking place in New Orleans on February 15th & 16th of 2018. For more information and to register visit: http://clojuresync.com/.LambdaDays 2018 will be taking place February 22nd and 23rd in Kraków, Poland. For more information, and to register, visit http://www.lambdadays.org/.If you have a conference related to functional programming, contact me, and I will be happy to announce it.AnnouncementsSome of you have asked how you can support Functional Geekery, in that vein,Functional Geekery now has a Patreon Page.If that is one of the ways you would like to show your support, you canfind out more at https://www.patreon.com/fngeekery.Topics [@About DavidIdrisIndiana University BloomingtonRacketType Driven Development in IdrisThe Type Theory PodcastDan Friedman on Functional GeekeryDavid’s introduction to programming and computersMS-DOS GW-BASICMajor in Philosophy with Minor in Computer ScienceWhat put functional programming on David’s radarLispHaskellA Gentle Introduction to HaskellStructure and Interpretation of Computer ProgramsPLTScheme, now RacketInternship doing I.T.QBasicCPerlSmalltalkDavid’s grad school workExposure to Idris at St Andrew’s summer schoolGeneral ML exposure around CopenhagenFalse dichotomy between industry and “academic” languagesProgression to push into dependent types“Part of my job description at the time was: learn about interesting things”The Type Theory PodcastSoftware FoundationsAdam Chlipala on Functional GeekeryDependent Types as a aesthetic thingType Driven DevelopmentInteractive programming environments from the 80’s“Let the computer do what the computer is good at, which is the details”NuprlJon Sterling’s jonPRL and RedPRLTypes as predicates that describe behaviorAgdaCoqTyped RacketUsing Racket as a proof language for Nuprl type systemLogic for Computable Functions by Dana S. ScottRobin MilnerEdinburgh LCFMLRunning LCF style proofs in Racket macro-expansionHackettcurminiKanrenµKanrenScribbleSlideshowvideoResources to get started understanding dependent typesSoftware FoundationsUpcoming _Little Schemer_ family book on dependent types with Dan FriedmanLittle SchemerUpcoming talks previewing book at RacketCon and CodeMeshOregon Programming Languages Summer School videosSuggestions for a title in Little Schemer traditionAs always, a giant Thank You goes to David Belcher for the logo design.