Blogs about: Hoas
Featured Blog
Reasoning on an imperative object based calculus in higher-order abstract syntax
By Alberto Ciaffaglione, Luigi Liquori and Marino Miculan, from MERLIN 2003, available from Luigi Liquori’s website: We illustrate the benefits of using Natural Deduction in combination with wea… more →
Name binding blog
Reasoning on an imperative object based calculus in higher-order abstract syntax
Name Binding Admin wrote 2 days ago: By Alberto Ciaffaglione, Luigi Liquori and Marino Miculan, from MERLIN 2003, available from Luigi Li … more →
Programming with proofs and explicit contexts
Name Binding Admin wrote 2 weeks ago: By Brigitte Pientka and Johua Dunfield, from PPDP 2008, available from the Beluga website: This pape … more →
Higher-order abstract syntax with induction in Isabelle/HOL: formalizing the pi-calculus and mechanizing the Theory of Contexts
Name Binding Admin wrote 2 weeks ago: By Christine Roeckl, Daniel Hirchskoff and Stefan Berghofer, from FOSSACS 2001, available from Chris … more →
Combining de Bruijn indices and higher-order abstract syntax in Coq
Name Binding Admin wrote 3 weeks ago: Sorry for the long delay in posting any updates. This last week, I was invited to give a talk in Su … more →
Abstracting syntax
Name Binding Admin wrote 1 month ago: By Brian Aydemir, Stephan A. Zdancewic and Stephanie Weirich, University of Pennsylvania Technical R … more →
Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism
Name Binding Admin wrote 1 month ago: By Geoffrey Washburn and Stephanie Weirich, from ICFP 2003, available from Stephanie Weirich’s … more →
Nominal abstract syntax vs. higher-order abstract syntax
— 2 comments
Name Binding Admin wrote 1 month ago: This blog post is a little different from the rest, as it considers two articles from the SIGACT Log … more →
Focusing and higher-order abstract syntax
Name Binding Admin wrote 1 month ago: By Noam Zeilberger, from POPL 2008, available from Noam Zeilberger’s website: Focusing is a pr … more →
Ahead of the Curve
— 1 comment
pawsinsd wrote 1 month ago: We have two small decks, one off the living room and another off the master bedroom. A few weeks ago … more →
Higher-order abstract syntax
Name Binding Admin wrote 1 month ago: By Frank Pfenning and Conal Elliott, from SLDI 88, available from Frank Pfenning’s website: We … more →
Condos, HOAs and FHAs –More doom and gloom to come?
Gaby wrote 2 months ago: Does your HOA have a Reserve Study? Does your HOA have adequate reserves? Why are single family resi … more →
Practical programming with higher-order encodings and dependent types
Name Binding Admin wrote 2 months ago: By Adam Poswolsky and Carsten Schurmann, from ESOP 2008, available from the Delphin website: Higher- … more →
klassy like a kappa
— 1 comment
Shanna wrote 2 months ago: I only know one person who understands that kappa thing. I am too lazy to type: I should really NEVE … more →
An overview of λProlog
— 2 comments
Name Binding Admin wrote 2 months ago: By Gopalan Nadathur and Dale Miller, from ICLP 88, available from the λProlog website: λProlog is a … more →
Your Freedom Stops Where the HOA Begins
Dindy wrote 2 months ago: Not content to go after junk cars and unmown lawns, Homeowner’s Associations have decided that … more →
On the role of names in reasoning about lambda-tree syntax specifications
Name Binding Admin wrote 2 months ago: Alwen Tiu, from LFMTP 2008, available from Alwen Tiu’s website. Lambda tree syntax (a variant … more →
Syntax for free: representing syntax with binding using parametricity
— 1 comment
Name Binding Admin wrote 2 months ago: Robert Atkey, from TLCA 2009, available from Robert Atkey’s website. We show that, in a parame … more →
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
— 4 comments
Name Binding Admin wrote 2 months ago: Brigitte Pientka, from POPL 2008, available from Brigitte Pientka’s website. Higher-order abst … more →
Parametric higher-order abstract syntax
— 2 comments
Name Binding Admin wrote 3 months ago: Adam Chlipala, from ICFP 2008, available from Adam Chlipala’s website: We present parametric h … more →
