BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
higher-order
Google higher-order

Tag #higher-order

801 papers:

POPLPOPL-2020-ArntzeniusK #evaluation #functional
Seminaïve evaluation for a higher-order functional language (MA, NK), p. 28.
POPLPOPL-2020-DahlqvistK #probability #semantics #source code
Semantics of higher-order probabilistic programs with conditioning (FD, DK), p. 29.
POPLPOPL-2020-Jaber #automation #equivalence #named #source code
SyTeCi: automating contextual equivalence for higher-order programs with references (GJ), p. 28.
CSLCSL-2020-HoelzelW #logic #on the #semantics
On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics (MH, RW), p. 16.
FSCDFSCD-2019-0001K #polymorphism #termination
Polymorphic Higher-Order Termination (LC0, CK), p. 18.
FSCDFSCD-2019-AhrensHLM #composition #monad #specification
Modular Specification of Monads Through Higher-Order Presentations (BA, AH, AL, MM), p. 19.
FSCDFSCD-2019-CernaK #framework
A Generic Framework for Higher-Order Generalizations (DMC, TK), p. 19.
ICFP-2019-KissFEJ #haskell #programming
Higher-order type-level programming in Haskell (CK, TF, SE, SPJ), p. 26.
CIKMCIKM-2019-Wang0CRR #algorithm #parallel #performance
Efficient Sequential and Parallel Algorithms for Estimating Higher Order Spectra (ZW, AAM0, XC, NR, SR), pp. 1743–1752.
ICMLICML-2019-Abu-El-HaijaPKA #architecture #graph #named
MixHop: Higher-Order Graph Convolutional Architectures via Sparsified Neighborhood Mixing (SAEH, BP, AK, NA, KL, HH, GVS, AG), pp. 21–29.
ICMLICML-2019-BansalLRSW #logic #machine learning #named #proving #theorem proving
HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving (KB, SML, MNR, CS, SW), pp. 454–463.
ICMLICML-2019-LiZT
Alternating Minimizations Converge to Second-Order Optimal Solutions (QL, ZZ, GT), pp. 3935–3943.
ICMLICML-2019-LuHW #convergence #named #optimisation
PA-GD: On the Convergence of Perturbed Alternating Gradient Descent to Second-Order Stationary Points for Structured Nonconvex Optimization (SL, MH, ZW), pp. 4134–4143.
ICMLICML-2019-PanageasPW #algorithm #convergence #distributed #multi #optimisation
Multiplicative Weights Updates as a distributed constrained optimization algorithm: Convergence to second-order stationary points almost always (IP, GP, XW), pp. 4961–4969.
ICMLICML-2019-SinglaWFF #approximate #comprehension #learning
Understanding Impacts of High-Order Loss Approximations and Features in Deep Learning Interpretation (SS0, EW, SF, SF), pp. 5848–5856.
KDDKDD-2019-LiST #classification #markov #multi #network #predict #random
Multi-task Recurrent Neural Networks and Higher-order Markov Random Fields for Stock Price Movement Prediction: Multi-task RNN and Higer-order MRFs for Stock Price Classification (CL, DS, DT), pp. 1141–1151.
OOPSLAOOPSLA-2019-NearDASGWSZSSS #difference #linear #named #privacy #type system
Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy (JPN, DD, CA, TS, PG, LW, NS, MZ0, NS, AS, DS), p. 30.
PEPMPEPM-2019-SatoI0 #model checking #refinement #type inference
Combining higher-order model checking with refinement type inference (RS, NI, NK0), pp. 47–53.
PEPMPEPM-2019-WatanabeTO0 #reduction #source code #verification
Reduction from branching-time property verification of higher-order programs to HFL validity checking (KW, TT, HO, NK0), pp. 22–34.
PLDIPLDI-2019-NguyenGTH #contract #source code #termination
Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs (PCN, TG, STH, DVH), pp. 845–859.
POPLPOPL-2019-BizjakGKB #concurrent #logic #named
Iron: managing obligations in higher-order concurrent separation logic (AB, DG, RK, LB), p. 30.
POPLPOPL-2019-SatoABGGH #approximate #convergence #optimisation #probability #reasoning #source code #verification
Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization (TS, AA0, GB, MG, DG0, JH), p. 30.
PPDPPPDP-2019-Kobayashi #model checking
10 Years of the Higher-Order Model Checking Project (Extended Abstract) (NK0), p. 2.
SASSAS-2019-OkuyamaT0 #functional #logic #source code
A Temporal Logic for Higher-Order Functional Programs (YO, TT, NK0), pp. 437–458.
ESOPESOP-2019-FuhsK #dependence #framework
A Static Higher-Order Dependency Pair Framework (CF, CK), pp. 752–782.
CADECADE-2019-BarbosaROTB #logic #smt
Extending SMT Solvers to Higher-Order Logic (HB, AR, DEO, CT, CWB), pp. 35–54.
ICSMEICSME-2018-0006LEL #feature model #interactive #predict
Predicting Higher Order Structural Feature Interactions in Variable Systems (SF0, LL, AE, RELH), pp. 252–263.
FSCDFSCD-2018-CernaK #anti #equation
Higher-Order Equational Pattern Anti-Unification (DMC, TK), p. 17.
FSCDFSCD-2018-Vignudelli #equivalence #probability #proving
Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages (Invited Talk) (VV), p. 2.
ICFP-2018-ElsmanHAO #functional #gpu #in the large #programming
Static interpretation of higher-order modules in Futhark: functional GPU programming in the large (ME, TH, DA, CEO), p. 30.
ICFP-2018-StampoulisC #functional #learning #logic programming #prolog #prototype #using
Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam (AS, AC), p. 30.
CIKMCIKM-2018-ANR #algorithm #generative #scalability #using
A Scalable Algorithm for Higher-order Features Generation using MinHash (PA, NN, RR), pp. 1213–1222.
ICMLICML-2018-DunnerLGBHJ #algorithm #distributed #trust
A Distributed Second-Order Algorithm You Can Trust (CD, AL, MG, AB, TH, MJ), pp. 1357–1365.
ICMLICML-2018-HongRL #algorithm #distributed #network #optimisation
Gradient Primal-Dual Algorithm Converges to Second-Order Stationary Solution for Nonconvex Distributed Optimization Over Networks (MH, MR, JDL), pp. 2014–2023.
ICMLICML-2018-JiaoV #kernel #permutation
The Weighted Kendall and High-order Kernels for Permutations (YJ, JPV), pp. 2319–2327.
ICMLICML-2018-MorvanV #algorithm #interactive #modelling #named #set
WHInter: A Working set algorithm for High-dimensional sparse second order Interaction models (MLM, JPV), pp. 3632–3641.
ICMLICML-2018-SongSE
Accelerating Natural Gradient with Higher-Order Invariance (YS, JS, SE), pp. 4720–4729.
ICPRICPR-2018-ChengSZW0 #image #retrieval
Deep High-order Supervised Hashing for Image Retrieval (JC, QS, JZ, XW, QZ0), pp. 2693–2698.
ICPRICPR-2018-RoyT #learning #using
Learning to Learn Second-Order Back-Propagation for CNNs Using LSTMs (AR, ST), pp. 97–102.
ICPRICPR-2018-ZhouXZH #graph #multi #online
Online Multi-Target Tracking with Tensor-Based High-Order Graph Matching (ZZ, JX, MZ, WH), pp. 1809–1814.
KDDKDD-2018-Lian0ZGCT0 #network #proximity
High-order Proximity Preserving Information Network Hashing (DL, KZ0, VWZ, YG, LC, IWT, XX0), pp. 1744–1753.
OOPSLAOOPSLA-2018-SelakovicPKT #generative #testing
Test generation for higher-order functions in dynamic languages (MS, MP, RK, FT), p. 27.
LOPSTRLOPSTR-2018-TroumpoukisC #logic programming #source code
Predicate Specialization for Definitional Higher-Order Logic Programs (AT, AC), pp. 132–147.
PADLPADL-2018-BiermannDS #functional #source code #spreadsheet
Rewriting High-Level Spreadsheet Structures into Higher-Order Functional Programs (FB, WD, PS), pp. 20–35.
POPLPOPL-2018-0001ST #nondeterminism #refinement #source code #type system #verification
Relatively complete refinement type system for verification of higher-order non-deterministic programs (HU0, YS, TT), p. 29.
POPLPOPL-2018-BernardyBNJS #haskell #linear #polymorphism
Linear Haskell: practical linearity in a higher-order polymorphic language (JPB, MB, RRN, SPJ, AS), p. 29.
POPLPOPL-2018-BurnOR #horn clause #verification
Higher-order constrained horn clauses for verification (TCB, CHLO, SJR), p. 28.
POPLPOPL-2018-ClairambaultGM #recursion
Linearity in higher-order recursion schemes (PC, CG, ASM), p. 29.
POPLPOPL-2018-EhrhardPT #probability #programming
Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming (TE, MP, CT), p. 28.
POPLPOPL-2018-Kuncar0 #safety
Safety and conservativity of definitions in HOL and Isabelle/HOL (OK, AP0), p. 26.
POPLPOPL-2018-NguyenGTH #contract #source code #verification
Soft contract verification for higher-order stateful programs (PCN, TG, STH, DVH), p. 30.
POPLPOPL-2018-ScibiorKVSYCOMH #validation
Denotational validation of higher-order Bayesian inference (AS, OK, MV, SS, HY, YC, KO, SKM, CH, ZG), p. 29.
PPDPPPDP-2018-Terao #abstraction #lazy evaluation #verification
Lazy Abstraction for Higher-Order Program Verification (TT), p. 13.
ASEASE-2018-NagashimaH #named #proving #recommendation
PaMpeR: proof method recommendation system for Isabelle/HOL (YN, YH), pp. 362–372.
ESEC-FSEESEC-FSE-2018-MechtaevGCR #constraints #execution #symbolic computation
Symbolic execution with existential second-order constraints (SM, AG, AC, AR), pp. 389–399.
ESEC-FSEESEC-FSE-2018-WongMK #automation #configuration management #execution #mutation testing #program repair #testing
Beyond testing configurable systems: applying variational execution to automatic program repair and higher order mutation testing (CPW, JM, CK), pp. 749–753.
ESOPESOP-2018-0001TW #model checking #verification
Higher-Order Program Verification via HFL Model Checking (NK0, TT, KW), pp. 711–738.
ESOPESOP-2018-HupelN #compilation
A Verified Compiler from Isabelle/HOL to CakeML (LH, TN), pp. 999–1026.
CAVCAV-2018-Satake0 #functional #logic #source code
Propositional Dynamic Logic for Higher-Order Functional Programs (YS, HU0), pp. 105–123.
CSLCSL-2018-FerrarottiBV #logic #transitive
Expressivity Within Second-Order Transitive-Closure Logic (FF, JVdB, JV), p. 18.
CSLCSL-2018-MadhusudanMS0 #decidability #logic #synthesis
A Decidable Fragment of Second Order Logic With Applications to Synthesis (PM, UM, SS, MV0), p. 19.
CSLCSL-2018-Terui #logic
MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics (KT), p. 19.
IJCARIJCAR-2018-BentkampBCW #logic
Superposition for Lambda-Free Higher-Order Logic (AB, JCB, SC, UW), pp. 28–46.
IJCARIJCAR-2018-SteenB #proving
The Higher-Order Prover Leo-III (AS, CB), pp. 108–116.
TAPTAP-2018-Keller #bound #testing #verification
Tactic Program-Based Testing and Bounded Verification in Isabelle/HOL (CK), pp. 103–119.
AFLAFL-2017-CrespiReghizziP #precedence
Higher-order Operator Precedence Languages (SCR, MP), pp. 86–100.
FSCDFSCD-2017-BlanchetteFT #multi
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL (JCB, MF, DT), p. 18.
FSCDFSCD-2017-Gaboardi #relational #source code #type system #verification
Type Systems for the Relational Verification of Higher Order Programs (Invited Talk) (MG), p. 1.
FSCDFSCD-2017-SuzukiF0T #automaton #model checking #recursion
Streett Automata Model Checking of Higher-Order Recursion Schemes (RS0, KF, NK0, TT), p. 18.
IFM-2017-Linker #reasoning #safety
Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL (SL), pp. 34–49.
IFM-2017-RizaldiKHFIAHN #formal method #monitoring
Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL (AR, JK, MH, JF, FI, MA, EH, TN), pp. 50–66.
ICFP-2017-AguirreBG0S #logic #relational #source code
A relational logic for higher-order programs (AA0, GB, MG, DG0, PYS), p. 29.
ICFP-2017-Hamana #algebra #calculus #decidability #how
How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation (MH), p. 28.
ICFP-2017-MelgrattiP #contract
Chaperone contracts for higher-order sessions (HCM, LP), p. 29.
ICFP-2017-WayeCD #contract #named
Whip: higher-order contracts for modern services (LW, SC, CD), p. 28.
ICMLICML-2017-ArjevaniS #complexity #problem
Oracle Complexity of Second-Order Methods for Finite-Sum Problems (YA, OS), pp. 205–213.
ICMLICML-2017-CalandrielloLV #adaptation #kernel #online #optimisation #sketching
Second-Order Kernel Online Convex Optimization with Adaptive Sketching (DC, AL, MV), pp. 645–653.
ICMLICML-2017-SuzumuraNUTT #interactive #modelling
Selective Inference for Sparse High-Order Interaction Models (SS, KN, YU, KT, IT), pp. 3338–3347.
KDDKDD-2017-WuG #markov #process
Retrospective Higher-Order Markov Processes for User Trails (TW, DFG), pp. 1185–1194.
KDDKDD-2017-Xu0TTL #distance #named #optimisation #rating #recommendation
HoORaYs: High-order Optimization of Rating Distance for Recommender Systems (JX0, YY0, HT, XT, JL0), pp. 525–534.
KDDKDD-2017-YinBLG #clustering #graph
Local Higher-Order Graph Clustering (HY, ARB, JL, DFG), pp. 555–564.
ECOOPECOOP-2017-SaleilF #interprocedural #static analysis
Interprocedural Specialization of Higher-Order Dynamic Languages Without Static Analysis (BS, MF), p. 23.
PADLPADL-2017-HedgesOSWZ #game studies
Selection Equilibria of Higher-Order Games (JH, PO, ES, VW, PZ), pp. 136–151.
PEPMPEPM-2017-KlinikHJP #predict #workflow
Predicting resource consumption of higher-order workflows (MK, JH, JMJ, RP), pp. 99–110.
PEPMPEPM-2017-SuwaT0I #code generation #model checking #verification
Verification of code generators via higher-order model checking (TS, TT, NK0, AI), pp. 59–70.
POPLPOPL-2017-DAntoniV #finite #logic #monad #sequence
Monadic second-order logic on finite sequences (LD, MV), pp. 232–245.
POPLPOPL-2017-KobayashiLB #fixpoint #logic #on the #recursion
On the relationship between higher-order recursion schemes and higher-order fixpoint logic (NK0, ÉL, FB), pp. 246–259.
POPLPOPL-2017-KrebbersTB #concurrent #interactive #logic #proving
Interactive proofs in higher-order concurrent separation logic (RK, AT, LB), pp. 205–217.
POPLPOPL-2017-Krogh-Jespersen #concurrent #logic #relational
A relational model of types-and-effects in higher-order concurrent separation logic (MKJ, KS, LB), pp. 218–231.
POPLPOPL-2017-MadhavanKK #contract #verification
Contract-based resource verification for higher-order functions with memoization (RM, SK, VK), pp. 330–343.
PPDPPPDP-2017-Sabel
Alpha-renaming of higher-order meta-expressions (DS), pp. 151–162.
CASECASE-2017-LiuJXX #performance #probability
Fast terminal sliding mode control of high-order stochastic systems (XL, XJ, LX, HX), pp. 1592–1597.
CASECASE-2017-WangW #approach #constraints #programming #using
Resolve reactive robot control with perturbed constraints using a second order cone programming approach (YW, LW), pp. 124–129.
ESOPESOP-2017-KopS #complexity #nondeterminism #power of #programming #using
The Power of Non-determinism in Higher-Order Implicit Complexity - Characterising Complexity Classes Using Non-deterministic Cons-Free Programming (CK, JGS), pp. 668–695.
ESOPESOP-2017-Krebbers0BJDB #concurrent #logic
The Essence of Higher-Order Concurrent Separation Logic (RK, RJ0, AB, JHJ, DD, LB), pp. 696–723.
ESOPESOP-2017-Kuncar0 #consistency
Comprehending Isabelle/HOL's Consistency (OK, AP0), pp. 724–749.
ESOPESOP-2017-Sato0 #composition #functional #source code #verification
Modular Verification of Higher-Order Functional Programs (RS, NK0), pp. 831–854.
ESOPESOP-2017-TassarottiJ0 #concurrent #logic #refinement
A Higher-Order Logic for Concurrent Termination-Preserving Refinement (JT, RJ0, RH0), pp. 909–936.
CADECADE-2017-BeckerBWW
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms (HB, JCB, UW, DW), pp. 432–453.
CADECADE-2017-NagashimaK #generative #proving
A Proof Strategy Language and Proof Script Generation for Isabelle/HOL (YN, RK), pp. 528–545.
FSCDFSCD-2016-Hamana #algebra #category theory #normalisation
Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories (MH), p. 18.
FSCDFSCD-2016-Hasuo #algebra #approach
Coalgebras and Higher-Order Computation: a GoI Approach (IH), p. 2.
FSCDFSCD-2016-KopS #complexity
Complexity Hierarchies and Higher-Order Cons-Free Rewriting (CK, JGS), p. 18.
FSCDFSCD-2016-LibalM #unification
Functions-as-Constructors Higher-Order Unification (TL, DM0), p. 17.
ICFP-2016-0002KBD
Higher-order ghost state (RJ0, RK, LB, DD), pp. 256–269.
ICFP-2016-WatanabeST0 #automation #functional #source code #termination
Automatically disproving fair termination of higher-order functional programs (KW, RS, TT, NK0), pp. 243–255.
ICPRICPR-2016-BulatovKR #energy #generative
Energy minimization of discrete functions with higher-order potentials for depth map generation (DB, BK, FR), pp. 2344–2349.
ICPRICPR-2016-FukanoMISSI #energy #image #re-engineering
Room reconstruction from a single spherical image by higher-order energy minimization (KF, YM, SI, ESS, AS, HI0), pp. 1768–1773.
ICPRICPR-2016-NaminAP #2d #3d #segmentation #semantics #using
2D-3D semantic segmentation using cardinality as higher-order loss (SRN, JMA, LP), pp. 3775–3780.
KDDKDD-2016-ZhouVBJD #online
Accelerating Online CP Decompositions for Higher Order Tensors (SZ0, XVN, JB0, YJ, ID), pp. 1375–1384.
ECOOPECOOP-2016-PalmerS #program analysis
Higher-Order Demand-Driven Program Analysis (ZP, SFS0), p. 25.
LOPSTRLOPSTR-2016-Schmidt-Schauss #recursion #unification
Nominal Unification of Higher Order Expressions with Recursive Let (MSS, TK, JL, MV), pp. 328–344.
PLDIPLDI-2016-MalekiYB
Higher-order and tuple-based massively-parallel prefix sums (SM, AY, MB), pp. 539–552.
POPLPOPL-2016-HagueKO #automaton #bound
Unboundedness and downward closures of higher-order pushdown automata (MH, JK, CHLO), pp. 151–163.
POPLPOPL-2016-JiaGP #monitoring
Monitors and blame assignment for higher-order session types (LJ, HG, FP), pp. 582–594.
POPLPOPL-2016-MuraseT0SU #functional #source code #verification
Temporal verification of higher-order functional programs (AM, TT, NK0, RS, HU0), pp. 57–68.
POPLPOPL-2016-SangiorgiV #bisimulation #probability
Environmental bisimulations for probabilistic higher-order languages (DS, VV), pp. 595–607.
PPDPPPDP-2016-CharalambidisRT #logic programming #representation
Higher-order logic programming: an expressive language for representing qualitative preferences (AC, PR, AT), pp. 24–37.
ESOPESOP-2016-KouzapasPY #on the #process
On the Relative Expressiveness of Higher-Order Session Processes (DK, JAP, NY), pp. 446–475.
ESOPESOP-2016-Lochbihler #encryption #logic #probability
Probabilistic Functions and Cryptographic Oracles in Higher Order Logic (AL), pp. 503–531.
ESOPESOP-2016-WangN #approach #functional #source code #syntax
A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (YW, GN), pp. 752–779.
CSLCSL-2016-KotekVZ #bound #finite #monad #satisfiability
Monadic Second Order Finite Satisfiability and Unbounded Tree-Width (TK, HV, FZ), p. 20.
ICSTICST-2016-TokumotoYSH #analysis #c #mutation testing #named #virtual machine
MuVM: Higher Order Mutation Analysis Virtual Machine for C (ST, HY, KS, SH), pp. 320–329.
IJCARIJCAR-2016-HupelK #scala #source code
Translating Scala Programs to Isabelle/HOL - System Description (LH, VK), pp. 568–577.
WICSAWICSA-2015-BangM #design #detection
Proactive Detection of Higher-Order Software Design Conflicts (JYB, NM), pp. 155–164.
JCDLJCDL-2015-CuongCKL #documentation #information management #performance #using
Scholarly Document Information Extraction using Extensible Features for Efficient Higher Order Semi-CRFs (NVC, MKC, MYK, WSL), pp. 61–64.
ICALPICALP-v2-2015-MichalewskiM #logic #monad #quantifier
Baire Category Quantifier in Monadic Second Order Logic (HM, MM), pp. 362–374.
ICFPICFP-2015-AvanziniLM #complexity #first-order #functional #source code
Analysing the complexity of functional programs: higher-order meets first-order (MA, UDL, GM), pp. 152–164.
ICFPICFP-2015-KeilT #contract
Blame assignment for higher-order contracts with intersection and union (MK, PT), pp. 375–386.
ICFPICFP-2015-NeisHKMDV #compilation #imperative #named
Pilsner: a compositionally verified compiler for a higher-order imperative language (GN, CKH, JOK, CM, DD, VV), pp. 166–178.
FDGFDG-2015-LongstreetCB #education #game studies
Invoking Higher Orders of Thinking in Serious Educational Games (CSL, KMLC, DB).
KDDKDD-2015-CaiTFJH #mining #named #performance
Facets: Fast Comprehensive Mining of Coevolving High-order Time Series (YC, HT, WF, PJ, QH), pp. 79–88.
ECOOPECOOP-2015-KeilT #contract #named
TreatJS: Higher-Order Contracts for JavaScripts (MK, PT), pp. 28–51.
PEPMPEPM-2015-BransenDS #evaluation #incremental
Incremental Evaluation of Higher Order Attributes (JB, AD, SDS), pp. 39–48.
PEPMPEPM-2015-KootH #analysis #exception #functional #semantics #strict #type system
Type-based Exception Analysis for Non-strict Higher-order Functional Languages with Imprecise Exception Semantics (RK, JH), pp. 127–138.
PEPMPEPM-2015-VerstoepH #analysis #functional #strict
Polyvariant Cardinality Analysis for Non-strict Higher-order Functional Languages: Brief Announcement (HV, JH), pp. 139–142.
PLDIPLDI-2015-NguyenH #source code
Relatively complete counterexamples for higher-order programs (PCN, DVH), pp. 446–456.
POPLPOPL-2015-BartheGAHRS #approximate #design #difference #privacy #refinement #relational
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy (GB, MG, EJGA, JH, AR, PYS), pp. 55–68.
PPDPPPDP-2015-StievenartNMR #abstract interpretation #concurrent #debugging #detection #source code
Detecting concurrency bugs in higher-order programs through abstract interpretation (QS, JN, WDM, CDR), pp. 232–243.
ICSEICSE-v1-2015-MilicevicNKJ #constraints #relational #theorem proving
Alloy*: A General-Purpose Higher-Order Relational Constraint Solver (AM, JPN, EK, DJ), pp. 609–619.
CGOCGO-2015-LeissaKH #graph #representation
A graph-based higher-order intermediate representation (RL, MK, SH), pp. 202–212.
CADECADE-2015-Libal #unification
Regular Patterns in Second-Order Unification (TL), pp. 557–571.
CADECADE-2015-MaricJM #correctness #proving #using
Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 (FM, PJ, MM), pp. 256–271.
CAVCAV-2015-KuwaharaSU0 #abstraction #functional #source code #termination
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs (TK, RS, HU, NK), pp. 287–303.
CSLCSL-2015-Berardi #comprehension #induction
Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness (SB), pp. 343–358.
CSLCSL-2015-GrelloisM #linear #logic #model checking #relational #semantics
Relational Semantics of Linear Logic and Higher-order Model Checking (CG, PAM), pp. 260–276.
CSLCSL-2015-SalvatiW #behaviour #source code
A Model for Behavioural Properties of Higher-order Programs (SS, IW), pp. 229–243.
ICLPICLP-2015-Hallen #data mining #logic #mining #specification
Higher Order Support in Logic Specification Languages for Data Mining Applications (MvdH), pp. 330–336.
LICSLICS-2015-EnqvistSV #algebra #bisimulation #logic #monad
Monadic Second-Order Logic and Bisimulation Invariance for Coalgebras (SE, FS, YV), pp. 353–365.
LICSLICS-2015-Ong #model checking #overview #perspective
Higher-Order Model Checking: An Overview (LO), pp. 1–15.
SIGITESIGITE-2014-Kawash #logic #sql
Formulating second-order logic conditions in SQL (JK), pp. 115–120.
FMFM-2014-ZeydaSCS #composition #object-oriented
A Modular Theory of Object Orientation in Higher-Order UTP (FZ, TLVLS, AC, AS), pp. 627–642.
SEFMSEFM-2014-ArmstrongGS #lightweight #tool support #verification
Lightweight Program Construction and Verification Tools in Isabelle/HOL (AA, VBFG, GS), pp. 5–19.
ICFPICFP-2014-BergstromFLRS #effectiveness #optimisation
Practical and effective higher-order optimizations (LB, MF, ML, JHR, NS), pp. 81–93.
ICFPICFP-2014-KakiJ #analysis #framework #relational
A relational framework for higher-order shape analysis (GK, SJ), pp. 311–324.
IFLIFL-2014-FredrikssonGW #towards
Towards native higher-order remote procedure calls (OF, DRG, BW), p. 10.
GT-VMTGT-VMT-2014-DeckwerthV #constraints #generative #graph transformation
Generating Preconditions from Graph Constraints by Higher Order Graph Transformation (FD, GV).
ICGTICGT-2014-PoskittP #graph #monad #source code #verification
Verifying Monadic Second-Order Properties of Graph Programs (CMP, DP), pp. 33–48.
ICMLICML-c2-2014-LiZ #learning #problem
High Order Regularization for Semi-Supervised Learning of Structured Output Problems (YL, RSZ), pp. 1368–1376.
ICPRICPR-2014-GhoraiC #algorithm #composition #image #using
An Image Inpainting Algorithm Using Higher Order Singular Value Decomposition (MG, BC), pp. 2867–2872.
ICPRICPR-2014-LiYLMDWX #multi
Multiple-Output Regression with High-Order Structure Information (CL, LY, QL, FM, WD, YW, JX), pp. 3868–3873.
KDDKDD-2014-PurushothamMKO #feature model #interactive #learning #modelling
Factorized sparse learning models with interpretable high order feature interactions (SP, MRM, CCJK, RO), pp. 552–561.
KRKR-2014-CharalambidisR #logic programming
Constructive Negation in Extensional Higher-Order Logic Programming (AC, PR).
KRKR-2014-Lin14a #axiom #first-order #induction #semantics
A First-Order Semantics for Golog and ConGolog under a Second-Order Induction Axiom for Situations (FL).
SIGIRSIGIR-2014-ParkS #detection #modelling #probability
Second order probabilistic models for within-document novelty detection in academic articles (LAFP, SS), pp. 1103–1106.
PEPMPEPM-J-2013-WeijersHH14 #fault #polymorphism #security
Security type error diagnosis for higher-order, polymorphic languages (JW, JH, SH), pp. 200–218.
PLDIPLDI-2014-CaiGRO #difference #formal method #λ-calculus
A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation (YC, PGG, TR, KO), p. 17.
POPLPOPL-2014-Birkedal #composition #concurrent #imperative #reasoning #source code
Modular reasoning about concurrent higher-order imperative programs (LB), pp. 1–2.
POPLPOPL-2014-LagoSA #functional #induction #on the #probability #source code
On coinductive equivalences for higher-order probabilistic functional programs (UDL, DS, MA), pp. 297–308.
POPLPOPL-2014-PaganiSV #quantum #semantics
Applying quantitative semantics to higher-order quantum computing (MP, PS, BV), pp. 647–658.
POPLPOPL-2014-RamsayNO #abstraction #approach #model checking #refinement
A type-directed abstraction refinement approach to higher-order model checking (SJR, RPN, CHLO), pp. 61–72.
POPLPOPL-2014-SergeyVJ #analysis #composition #theory and practice
Modular, higher-order cardinality analysis in theory and practice (IS, DV, SLPJ), pp. 335–348.
PPDPPPDP-2014-StulovaMH #debugging #source code
Assertion-based Debugging of Higher-Order (C)LP Programs (NS, JFM, MVH), pp. 225–235.
ASEASE-2014-HarmanJMP #effectiveness #empirical #performance
Angels and monsters: an empirical investigation of potential test effectiveness and efficiency improvement from strongly subsuming higher order mutation (MH, YJ, PRM, MP), pp. 397–408.
SLESLE-J-2012-KrishnanW #analysis #attribute grammar #composition #termination
Monolithic and modular termination analyses for higher-order attribute grammars (LK, EVW), pp. 511–526.
ESOPESOP-2014-KuwaharaTU0 #automation #functional #source code #termination #verification
Automatic Termination Verification for Higher-Order Functional Programs (TK, TT, HU, NK), pp. 392–411.
ESOPESOP-2014-YoshimizuHFL #metric #proving #quantum
Measurements in Proof Nets as Higher-Order Quantum Circuits (AY, IH, CF, UDL), pp. 371–391.
FoSSaCSFoSSaCS-2014-KobayashiIT
Unsafe Order-2 Tree Languages Are Context-Sensitive (NK, KI, TT), pp. 149–163.
CAVCAV-2014-LeGQC #analysis
Shape Analysis via Second-Order Bi-Abduction (QLL, CG, SQ, WNC), pp. 52–68.
ICLPICLP-J-2014-CharalambidisER #logic programming #semantics
Minimum Model Semantics for Extensional Higher-order Logic Programming with Negation (AC, , PR), pp. 725–737.
IJCARIJCAR-2014-Lindblad #calculus #logic
A Focused Sequent Calculus for Higher-Order Logic (FL), pp. 61–75.
LICSLICS-CSL-2014-BernardoSV #interactive #on the #power of
On the discriminating power of passivation and higher-order interaction (MB, DS, VV), p. 10.
LICSLICS-CSL-2014-TsukadaO #composition #game studies #model checking
Compositional higher-order model checking via ω-regular games over Böhm trees (TT, CHLO), p. 10.
DRRDRR-2013-TaghvaPM #markov #modelling
Post processing with first- and second-order hidden Markov models (KT, SP, SM).
ICALPICALP-v1-2013-BohlerCKLPZ #complexity #diagrams #on the
On the Complexity of Higher Order Abstract Voronoi Diagrams (CB, PC, RK, CHL, EP, MZ), pp. 208–219.
LATALATA-2013-Ong #automaton #model checking #recursion
Recursion Schemes, Collapsible Pushdown Automata and Higher-Order Model Checking (LO), pp. 13–41.
RTARTA-2013-BaumgartnerKLV #anti
A Variant of Higher-Order Anti-Unification (AB, TK, JL, MV), pp. 113–127.
ICFPICFP-2013-AxelssonC #functional #source code #syntax #using
Using circular programs for higher-order syntax: functional pearl (EA, KC), pp. 257–262.
ICFPICFP-2013-BroadbentCHS #approach #named #verification
C-SHORe: a collapsible approach to higher-order verification (CHB, AC, MH, OS), pp. 13–24.
ICFPICFP-2013-Krishnaswami #functional #programming
Higher-order functional reactive programming without spacetime leaks (NRK), pp. 221–232.
ICFPICFP-2013-TuronDB #concurrent #hoare #logic #reasoning #refinement
Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency (AT, DD, LB), pp. 377–390.
GCMGCM-J-2012-Radke #graph #monad
HR* Graph Conditions Between Counting Monadic Second-Order and Second-Order Graph Formulas (HR).
HCIDHM-HB-2013-ZhaoLZ #analysis #statistics
Higher Order Statistics Analyses Based on the Mathematical Model of Surface Electromyography (YZ, DL, JZ), pp. 402–408.
ECOOPECOOP-2013-MaierO #incremental #programming
Higher-Order Reactive Programming with Incremental Lists (IM, MO), pp. 707–731.
ECOOPECOOP-2013-SvendsenBP #case study #composition #concurrent #library #named #specification
Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library (KS, LB, MJP), pp. 327–351.
PEPMPEPM-2013-SatoUK #model checking #scalability #source code #towards
Towards a scalable software model checker for higher-order programs (RS, HU, NK), pp. 53–62.
PEPMPEPM-2013-WeijersHH #fault #polymorphism #security
Security type error diagnosis for higher-order, polymorphic languages (JW, JH, SH), pp. 3–12.
PLDIPLDI-2013-SwamyWSCL #monad #source code #verification
Verifying higher-order programs with the dijkstra monad (NS, JW, CS, JC, BL), pp. 387–398.
POPLPOPL-2013-UnnoTK #automation #functional #source code #verification
Automating relatively complete verification of higher-order functional programs (HU, TT, NK), pp. 75–86.
PPDPPPDP-2013-WangCGN #reasoning #relational #specification
Reasoning about higher-order relational specifications (YW, KC, AG, GN), pp. 157–168.
ESEC-FSEESEC-FSE-2013-LiRSY #constraints #invariant
Second-order constraints in dynamic invariant inference (KL, CR, YS, MY), pp. 103–113.
SLESLE-2013-SoderbergH #attribute grammar
Circular Higher-Order Reference Attribute Grammars (ES, GH), pp. 302–321.
ASPLOSASPLOS-2013-XiangDLB #locality #named
HOTL: a higher order theory of locality (XX, CD, HL, BB), pp. 343–356.
CASECASE-2013-IsmailH #3d #anti #using
Trajectory tracking and anti-sway control of three-dimensional offshore boom cranes using second-order sliding modes (RMTRI, QPH), pp. 996–1001.
ESOPESOP-2013-KobayashiI #model checking #recursion #source code
Model-Checking Higher-Order Programs with Recursive Types (NK, AI), pp. 431–450.
ESOPESOP-2013-ToninhoCP #integration #monad #process
Higher-Order Processes, Functions, and Sessions: A Monadic Integration (BT, LC, FP), pp. 350–369.
FoSSaCSFoSSaCS-2013-BauerHK #monad #on the #parametricity
On Monadic Parametricity of Second-Order Functionals (AB, MH, AK), pp. 225–240.
FoSSaCSFoSSaCS-2013-Czajka #logic #recursion
Partiality and Recursion in Higher-Order Logic (LC0), pp. 177–192.
STOCSTOC-2013-KwokLLGT #algorithm #analysis #clustering #difference
Improved Cheeger’s inequality: analysis of spectral partitioning algorithms through higher order spectral gap (TCK, LCL, YTL, SOG, LT), pp. 11–20.
CSLCSL-2013-BroadbentK #model checking #recursion
Saturation-Based Model Checking of Higher-Order Recursion Schemes (CHB, NK), pp. 129–148.
LICSLICS-2013-AlurDT #monad #string #transducer
From Monadic Second-Order Definable String Transformations to Transducers (RA, ADG, AT), pp. 458–467.
LICSLICS-2013-KreutzerR #logic #monad
Quantitative Monadic Second-Order Logic (SK, CR), pp. 113–122.
VLDBVLDB-2012-AhmadKKN #named
DBToaster: Higher-order Delta Processing for Dynamic, Frequently Fresh Views (YA, OK, CK, MN), pp. 968–979.
RTARTA-2012-FuhsK #polynomial
Polynomial Interpretations for Higher-Order Rewriting (CF, CK), pp. 176–192.
FLOPSFLOPS-2012-Terauchi #automation #functional #source code #verification
Automated Verification of Higher-Order Functional Programs (TT), p. 2.
FLOPSFLOPS-2012-TobitaTK #analysis #model checking
Exact Flow Analysis by Higher-Order Model Checking (YT, TT, NK), pp. 275–289.
ICFPICFP-2012-EarlSMH #analysis #automaton #source code
Introspective pushdown analysis of higher-order programs (CE, IS, MM, DVH), pp. 177–188.
ICFPICFP-2012-LippmeierCKLJ #performance
Work efficient higher-order vectorisation (BL, MMTC, GK, RL, SLPJ), pp. 259–270.
ICFPICFP-2012-MyreenO #logic #ml #synthesis
Proof-producing synthesis of ML from higher-order logic (MOM, SO), pp. 115–126.
ICFPICFP-2012-NeatherwayRO #algorithm #model checking
A traversal-based algorithm for higher-order model checking (RPN, SJR, CHLO), pp. 353–364.
CIKMCIKM-2012-CamposDJN #approach #identification #named #web
GTE: a distributional second-order co-occurrence approach to improve the identification of top relevant dates in web snippets (RC, GD, AJ, CN), pp. 2035–2039.
ICPRICPR-2012-AlbarelliBRVT #graph #recognition #representation
A stable graph-based representation for object recognition through high-order matching (AA, FB, LR, SV, AT), pp. 3341–3344.
ICPRICPR-2012-HouZQ
Diffusion-driven high-order matching of partial deformable shapes (TH, MZ, HQ), pp. 137–140.
ICPRICPR-2012-MinKCK #approach #detection #using
A superpixel MRF approach using high-order likelihood for moving object detection (JM, HK, JC, ISK), pp. 266–269.
ICPRICPR-2012-RubioSLP #graph #image #representation
Image contextual representation and matching through hierarchies and higher order graphs (JCR, JS, AML, NP), pp. 2664–2667.
SIGIRSIGIR-2012-BenderskyC #dependence #information retrieval #modelling #query #using
Modeling higher-order term dependencies in information retrieval using query hypergraphs (MB, WBC), pp. 941–950.
OOPSLAOOPSLA-2012-Tobin-HochstadtH #contract #execution #symbolic computation
Higher-order symbolic execution via contracts (STH, DVH), pp. 537–554.
POPLPOPL-2012-KrishnaswamiBH #bound #functional #programming
Higher-order functional reactive programming in bounded space (NRK, NB, JH), pp. 45–58.
SASSAS-2012-Ledesma-GarzaR #analysis #functional #reachability #source code
Binary Reachability Analysis of Higher Order Functional Programs (RLG, AR), pp. 388–404.
SASSAS-2012-MadhavanRV #analysis #composition #source code
Modular Heap Analysis for Higher-Order Programs (RM, GR, KV), pp. 370–387.
LDTALDTA-2012-LinckeS #concept #object-oriented
From HOT to COOL: transforming higher-order typed languages to concept-constrained object-oriented languages (DL, SS), p. 3.
SLESLE-2012-KrishnanW #analysis #attribute grammar #termination
Termination Analysis for Higher-Order Attribute Grammars (LK, EVW), pp. 44–63.
CASECASE-2012-IsmailDH #using
Observer-based trajectory tracking for a class of underactuated Lagrangian systems using higher-order sliding modes (RMTRI, TDN, QPH), pp. 1204–1209.
DACDAC-2012-ZhangLWFW #performance #reduction
Fast nonlinear model order reduction via associated transforms of high-order volterra transfer functions (YZ, HL, QW, NF, NW), pp. 289–294.
STOCSTOC-2012-LeeGT #clustering #multi
Multi-way spectral partitioning and higher-order cheeger inequalities (JRL, SOG, LT), pp. 1117–1130.
CAVCAV-2012-HopkinsMO #equivalence #ml #named
Hector: An Equivalence Checker for a Higher-Order Fragment of ML (DH, ASM, CHLO), pp. 774–780.
CSLCSL-2012-BaillotL #complexity
Higher-Order Interpretations and Program Complexity (PB, UDL), pp. 62–76.
ICSTICST-2012-KintisPM #first-order
Isolating First Order Equivalent Mutants via Second Order Mutation (MK, MP, NM), pp. 701–710.
IJCARIJCAR-2012-Brown #automation #named #proving
Satallax: An Automatic Higher-Order Prover (CEB), pp. 111–117.
LICSLICS-2012-ElberfeldGT #first-order #logic #monad
Where First-Order and Monadic Second-Order Logic Coincide (ME, MG, TT), pp. 265–274.
LICSLICS-2012-EngelmannKS #first-order #model checking #monad
First-Order and Monadic Second-Order Model-Checking on Ordered Structures (VE, SK, SS), pp. 275–284.
LICSLICS-2012-PierardS #calculus #distributed
A Higher-Order Distributed Calculus with Name Creation (AP, ES), pp. 531–540.
LICSLICS-2012-TraytelPB #category theory #composition #data type #logic #proving #theorem proving
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (DT, AP, JCB), pp. 596–605.
VMCAIVMCAI-2012-CharltonHR #named #source code #verification
Crowfoot: A Verifier for Higher-Order Store Programs (NC, BH, BR), pp. 136–151.
VLDBVLDB-2011-VuB #evaluation #named
HOMES: A Higher-Order Mapping Evaluation System (HV, MB), pp. 1399–1402.
SCAMSCAM-2011-NicolayRMJ #automation #parallel #source code
Automatic Parallelization of Side-Effecting Higher-Order Scheme Programs (JN, CDR, WDM, VJ), pp. 185–194.
ICALPICALP-v2-2011-SalvatiW
Krivine Machines and Higher-Order Schemes (SS, IW), pp. 162–173.
RTARTA-2011-AotoYC #induction #theorem
Natural Inductive Theorems for Higher-Order Rewriting (TA, TY, YC), pp. 107–121.
RTARTA-2011-KopR #algebra #dependence #functional
Higher Order Dependency Pairs for Algebraic Functional Systems (CK, FvR), pp. 203–218.
RTARTA-2011-Roux #dependence #refinement
Refinement Types as Higher-Order Dependency Pairs (CR), pp. 299–312.
TLCATLCA-2011-AbelP #dependent type #unification
Higher-Order Dynamic Pattern Unification for Dependent Types and Records (AA, BP), pp. 10–26.
HaskellHaskell-2011-WestbrookFB #encoding #functional #haskell #library #programming language
Hobbits for Haskell: a library for higher-order encodings in functional programming languages (EMW, NF, PB), pp. 35–46.
ICFPICFP-2011-DisneyFM #contract
Temporal higher-order contracts (TD, CF, JM), pp. 176–188.
ICEISICEIS-v2-2011-JiaWLW #research
The Research on Stability of Supply Chain under High Order Delay (SJ, LW, CL, QW), pp. 361–367.
CIKMCIKM-2011-YanGC #learning #query #recommendation
Context-aware query recommendation by learning high-order relation in query logs (XY, JG, XC), pp. 2073–2076.
MLDMMLDM-2011-AidosF #clustering
Hierarchical Clustering with High Order Dissimilarities (HA, ALNF), pp. 280–293.
SEKESEKE-2011-Kaiser #concurrent #debugging #using
Constructing Subtle Concurrency Bugs Using Synchronization-Centric Second-Order Mutation Operators (LWGK), pp. 244–249.
BXBX-2011-Schmitt #π-calculus
Reversible Higher Order π Calculus (AS), p. 63.
PLDIPLDI-2011-Godefroid #generative #testing
Higher-order test generation (PG), pp. 258–269.
PLDIPLDI-2011-KobayashiSU #abstraction #model checking
Predicate abstraction and CEGAR for higher-order model checking (NK, RS, HU), pp. 222–233.
POPLPOPL-2011-OngR #algebra #data type #functional #pattern matching #source code #verification
Verifying higher-order functional programs with pattern-matching algebraic data types (CHLO, SJR), pp. 587–598.
PPDPPPDP-2011-InabaHHKN #logic #monad #using #verification
Graph-transformation verification using monadic second-order logic (KI, SH, ZH, HK, KN), pp. 17–28.
PPDPPPDP-2011-VirsedaM #composition #constraints #declarative #programming #semantics
A modular semantics for higher-order declarative programming with constraints (RdVV, FPM), pp. 41–52.
SASSAS-2011-MightH #abstract interpretation #concurrent #product line #source code #static analysis
A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs (MM, DVH), pp. 180–197.
ESEC-FSEESEC-FSE-2011-HarmanJL #generative #testing
Strong higher order mutation-based test data generation (MH, YJ, WBL), pp. 212–222.
SACSAC-2011-KaliszykU
Quotients revisited for Isabelle/HOL (CK, CU), pp. 1639–1644.
LDTALDTA-2011-EconomopoulosF #syntax
Higher-order transformations with nested concrete syntax (GRE, BF), p. 4.
ESOPESOP-2011-KoutavasH #encryption #testing
A Testing Theory for a Higher-Order Cryptographic Language — (VK, MH), pp. 358–377.
FoSSaCSFoSSaCS-2011-Kobayashi #algorithm #automaton #linear #model checking #recursion
A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes (NK0), pp. 260–274.
FoSSaCSFoSSaCS-2011-PierardS #bisimulation #calculus #distributed #process
Sound Bisimulations for Higher-Order Distributed Process Calculus (AP, ES), pp. 123–137.
CADECADE-2011-Brown #problem #proving #satisfiability #sequence #theorem proving
Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems (CEB), pp. 147–161.
CSLCSL-2011-DurandS #complexity #logic #problem #query
Enumeration Complexity of Logical Query Problems with Second-order Variables (AD, YS), pp. 189–202.
ISSTAISSTA-2011-TateishiPT #analysis #logic #monad #string
Path- and index-sensitive string analysis based on monadic second-order logic (TT, MP, OT), pp. 166–176.
LICSLICS-2011-BarrasJSW #decidability #first-order #named #type system
CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory (BB, JPJ, PYS, QW), pp. 143–151.
LICSLICS-2011-Clairambault #morphism
Isomorphisms of Types in the Presence of Higher-Order References (PC), pp. 152–161.
LICSLICS-2011-HasuoH #geometry #interactive #quantum #semantics
Semantics of Higher-Order Quantum Computation via Geometry of Interaction (IH, NH), pp. 237–246.
LICSLICS-2011-Kobayashi #model checking #theory and practice
Higher-Order Model Checking: From Theory to Practice (NK0), pp. 219–224.
PODSPODS-2010-BenediktPV #query
Positive higher-order queries (MB, GP, HV), pp. 27–38.
ICALPICALP-v2-2010-LanesePSS #calculus #communication #on the #process
On the Expressiveness of Polyadic and Synchronous Communication in Higher-Order Process Calculi (IL, JAP, DS, AS), pp. 442–453.
RTARTA-2010-AppelOS #composition
Higher-Order (Non-)Modularity (CA, VvO, JGS), pp. 17–32.
FLOPSFLOPS-2010-HaftmannN #code generation #term rewriting
Code Generation via Higher-Order Rewrite Systems (FH, TN), pp. 103–117.
ICFPICFP-2010-Crary #logic #representation
Higher-order representation of substructural logics (KC), pp. 131–142.
ICFPICFP-2010-DreyerNB #reasoning #relational
The impact of higher-order state and control effects on local relational reasoning (DD, GN, LB), pp. 143–156.
ICFPICFP-2010-HoldermansH #analysis #polymorphism
Polyvariant flow analysis with higher-ranked polymorphic types and higher-order effect operators (SH, JH), pp. 63–74.
ICGTICGT-2010-GadducciLV #calculus #semantics #μ-calculus
Counterpart Semantics for a Second-Order μ-Calculus (FG, ALL, AV), pp. 282–297.
ICPRICPR-2010-SemenovichS #performance
Tensor Power Method for Efficient MAP Inference in Higher-order MRFs (DS, AS), pp. 734–737.
ICPRICPR-2010-WangJHT #kernel #learning #multi
Multiple Kernel Learning with High Order Kernels (SW, SJ, QH, QT), pp. 2138–2141.
ICPRICPR-2010-ZhaoGC #image #recognition #representation
High-Order Circular Derivative Pattern for Image Representation and Recognition (SZ, YG, TC), pp. 2246–2249.
KEODKEOD-2010-ChanLB #automation #evolution #ontology #reasoning #representation
Higher-order Representation and Reasoning for Automated Ontology Evolution (MC, JL, AB), pp. 84–93.
ICMTICMT-2010-TisiCJ #atl
Improving Higher-Order Transformations Support in ATL (MT, JC, FJ), pp. 215–229.
PLEASEPLEASE-2010-KammullerRR #variability
Feature link propagation across variability representations with Isabelle/HOL (FK, AR, MOR), pp. 48–53.
OOPSLAOOPSLA-2010-KleinFF #random testing #source code #testing
Random testing for higher-order, stateful programs (CK, MF, RBF), pp. 555–566.
PEPMPEPM-2010-Haftmann #haskell #logic
From higher-order logic to Haskell: there and back again (FH), pp. 155–158.
POPLPOPL-2010-DreyerNRB #data type #logic #relational
A relational modal logic for higher-order stateful ADTs (DD, GN, AR, LB), pp. 185–198.
POPLPOPL-2010-JostHLH #resource management #source code
Static determination of quantitative resource usage for higher-order programs (SJ, KH, HWL, MH), pp. 223–236.
POPLPOPL-2010-KobayashiTU #multi #recursion #transducer #verification
Higher-order multi-parameter tree transducers and recursion schemes for program verification (NK, NT, HU), pp. 495–508.
PPDPPPDP-2010-Gacek #specification #syntax
Relating nominal and higher-order abstract syntax specifications (AG), pp. 177–186.
ESOPESOP-2010-NaumannB #bound #first-order #information management
Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions (DAN, AB), pp. 2–22.
FoSSaCSFoSSaCS-2010-Stirling #decidability
Introduction to Decidability of Higher-Order Matching (CS), p. 1.
TACASTACAS-2010-Aderhold #analysis #automation #recursion #source code #termination
Automated Termination Analysis for Programs with Second-Order Recursion (MA), pp. 221–235.
CSLCSL-2010-FioreH #equation #logic
Second-Order Equational Logic (MPF, CKH), pp. 320–335.
CSLCSL-2010-GanzowK #algorithm #induction #logic #monad
New Algorithm for Weak Monadic Second-Order Logic on Inductive Structures (TG, LK), pp. 366–380.
ICLPICLP-2010-Pahlavi10 #learning #logic
Higher-order Logic Learning and λ-Progol (NP), pp. 281–285.
IJCARIJCAR-2010-Aderhold #automation #axiom #induction #recursion #source code #synthesis
Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion (MA), pp. 263–277.
IJCARIJCAR-2010-BackesB #logic
Analytic Tableaux for Higher-Order Logic with Choice (JB, CEB), pp. 76–90.
IJCARIJCAR-2010-BlanchetteK
Monotonicity Inference for Higher-Order Formulas (JCB, AK), pp. 91–106.
LICSLICS-2010-KreutzerT #bound #complexity #logic #monad
Lower Bounds for the Complexity of Monadic Second-Order Logic (SK, ST), pp. 189–198.
ICALPICALP-v2-2009-BlumensathOW #bound #finite #monad #word
Boundedness of Monadic Second-Order Formulae over Finite Words (AB, MO, MW), pp. 67–78.
LATALATA-2009-Courcelle #algorithm #graph #logic #monad
Monadic Second-Order Logic for Graphs: Algorithmic and Language Theoretical Applications (BC), pp. 19–22.
TLCATLCA-2009-MostrousY #communication #mobile #optimisation #process
Session-Based Communication Optimisation for Higher-Order Mobile Processes (DM, NY), pp. 203–218.
TLCATLCA-2009-Strassburger #linear #logic #multi #proving
Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic (LS), pp. 309–324.
ICFPICFP-2009-ChlipalaMMSW #effectiveness #imperative #interactive #proving #source code
Effective interactive proofs for higher-order imperative programs (AC, JGM, GM, AS, RW), pp. 79–90.
HCIHCI-AUII-2009-TokosumiM #component
Extracting High-Order Aesthetic and Affective Components from Composer’s Writings (AT, HM), pp. 679–682.
ECIRECIR-2009-LlorenteR #automation #image #statistics #using
Using Second Order Statistics to Enhance Automated Image Annotation (AL, SMR), pp. 570–577.
ICMLICML-2009-DavisD #logic #markov
Deep transfer via second-order Markov logic (JD, PMD), pp. 217–224.
ICMLICML-2009-QianJZHW #random #sequence
Sparse higher order conditional random fields for improved sequence labeling (XQ, XJ, QZ, XH, LW), pp. 849–856.
ECMFAECMDA-FA-2009-TisiJFCB #model transformation #on the #using
On the Use of Higher-Order Model Transformations (MT, FJ, PF, SC, JB), pp. 18–33.
PEPMPEPM-2009-PardoFS #monad #source code
Shortcut fusion rules for the derivation of circular and higher-order monadic programs (AP, JPF, JS), pp. 81–90.
POPLPOPL-2009-JonssonN #call-by #supercompilation
Positive supercompilation for a higher order call-by-value language (PAJ, JN), pp. 277–288.
POPLPOPL-2009-Kobayashi #recursion #source code #verification
Types and higher-order recursion schemes for verification of higher-order programs (NK), pp. 416–428.
PPDPPPDP-2009-BentonKBH #program transformation #relational #semantics
Relational semantics for effect-based program transformations: higher-order store (NB, AK, LB, MH), pp. 301–312.
PPDPPPDP-2009-KaiserL #traversal
An Isabelle/HOL-based model of stratego-like traversal strategies (MK, RL), pp. 93–104.
PPDPPPDP-2009-Kobayashi #model checking
Model-checking higher-order functions (NK), pp. 25–36.
PPDPPPDP-2009-Virseda #algorithm #debugging #declarative #framework #logic #source code #verification
A higher-order logical framework for the algorithmic debugging and verification of declarative programs (RdVV), pp. 49–60.
CASECASE-2009-CaldwellM #estimation
Second-order optimal estimation of slip state for a simple slip-steered vehicle (TMC, TDM), pp. 133–139.
ESOPESOP-2009-LakinP #functional #induction #programming
Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming (MRL, AMP), pp. 47–61.
ESOPESOP-2009-SiekGT #design
Exploring the Design Space of Higher-Order Casts (JGS, RG, WT), pp. 17–31.
FASEFASE-2009-BruckerW
hol-TestGen (ADB, BW), pp. 417–420.
FoSSaCSFoSSaCS-2009-BroadbentO #model checking #on the #recursion
On Global Model Checking Trees Generated by Higher-Order Recursion Schemes (CHB, CHLO), pp. 107–121.
CADECADE-2009-SutcliffeBBT #automation #development #logic #proving #theorem proving
Progress in the Development of Automated Theorem Proving for Higher-Order Logic (GS, CB, CEB, FT), pp. 116–130.
CAVCAV-2009-HopkinsO #equivalence #model checking #named
Homer: A Higher-Order Observational Equivalence Model checkER (DH, CHLO), pp. 654–660.
CSLCSL-2009-Kreutzer #logic #monad #on the
On the Parameterised Intractability of Monadic Second-Order Logic (SK), pp. 348–363.
CSLCSL-2009-SchwinghammerBRY #hoare
Nested Hoare Triples and Frame Rules for Higher-Order Store (JS, LB, BR, HY), pp. 440–454.
LICSLICS-2009-KobayashiO #calculus #model checking #recursion #type system #μ-calculus
A Type System Equivalent to the Modal μ-Calculus Model Checking of Higher-Order Recursion Schemes (NK, CHLO), pp. 179–188.
VMCAIVMCAI-2009-DimoulasW #problem
The Higher-Order Aggregate Update Problem (CD, MW), pp. 44–58.
VLDBVLDB-2008-ZhangPWN #correlation #mining
Mining non-redundant high order correlations in binary data (XZ, FP, WW, ABN), pp. 1178–1188.
SCAMSCAM-2008-JiaH #fault #mutation testing #testing #using
Constructing Subtle Faults Using Higher Order Mutation Testing (YJ, MH), pp. 249–258.
WCREWCRE-2008-Muliawan #model transformation #transformation language #using
Extending a Model Transformation Language Using Higher Order Transformations (OM), pp. 315–318.
ICALPICALP-A-2008-Courcelle #aspect-oriented #graph #logic #monad
Graph Structure and Monadic Second-Order Logic: Language Theoretical Aspects (BC), pp. 1–13.
ICALPICALP-B-2008-BirkedalRSY #logic
A Simple Model of Separation Logic for Higher-Order Store (LB, BR, JS, HY), pp. 348–360.
RTARTA-2008-ArrighiD #algebra #confluence #encoding #λ-calculus
Linear-algebraic λ-calculus: higher-order, encodings, and confluence (PA, GD), pp. 17–31.
RTARTA-2008-LevyV #perspective #unification
Nominal Unification from a Higher-Order Perspective (JL, MV), pp. 246–260.
ICFPICFP-2008-Chlipala #parametricity #semantics #syntax
Parametric higher-order abstract syntax for mechanized semantics (AC), pp. 143–156.
CIKMCIKM-2008-AzzopardiV #evaluation #information management #named
Retrievability: an evaluation measure for higher order information access tasks (LA, VV), pp. 561–570.
ICPRICPR-2008-ChenCW #named #performance #using
HOPS: Efficient region labeling using Higher Order Proxy Neighborhoods (AYCC, JJC, LW), pp. 1–4.
ICPRICPR-2008-ParamanandR #geometry #performance
Efficient geometric matching with higher-order features (CP, ANR), pp. 1–4.
ICPRICPR-2008-ShenZL #detection #programming #using
Deformable surface stereo tracking-by-detection using Second Order Cone Programming (SS, YZ, YL), pp. 1–4.
ICPRICPR-2008-XiaoL #using
Improvement on Mean Shift based tracking using second-order information (LX, PL), pp. 1–4.
KDDKDD-2008-HuangDLL #clustering #equivalence
Simultaneous tensor subspace selection and clustering: the equivalence of high order svd and k-means clustering (HH, CHQD, DL, TL), pp. 327–335.
SIGIRSIGIR-2008-KeskustaloJPK #performance #visualisation
Intuition-supporting visualization of user’s performance based on explicit negative higher-order relevance (HK, KJ, AP, JK), pp. 675–682.
LOPSTRLOPSTR-2008-ArroyoRTV #approach #functional #source code
A Transformational Approach to Polyvariant BTA of Higher-Order Functional Programs (GA, JGR, ST, GV), pp. 40–54.
POPLPOPL-2008-Pientka #programming #syntax
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions (BP), pp. 371–382.
POPLPOPL-2008-Zeilberger #syntax
Focusing and higher-order abstract syntax (NZ), pp. 359–369.
PPDPPPDP-2008-ChitilD #algorithm #debugging #finite #functional #source code
Comprehending finite maps for algorithmic debugging of higher-order functional programs (OC, TD), pp. 205–216.
SACSAC-2008-LevadaMTS #estimation #parametricity #pseudo
Spatially non-homogeneous potts model parameter estimation on higher-order neighborhood systems by maximum pseudo-likelihood (ALML, NDAM, AT, DHPS), pp. 1733–1737.
SLESLE-2008-GorpKJ #integration #model transformation #transformation language
Transformation Language Integration Based on Profiles and Higher Order Transformations (PVG, AK, DJ), pp. 208–226.
DATEDATE-2008-FreuerJGN #constraints #design #on the #verification
On the Verification of High-Order Constraint Compliance in IC Design (JBF, GJ, JG, WN), pp. 26–31.
LCTESLCTES-2008-DelavalGP #automation #data flow #source code #type system
A type system for the automatic distribution of higher-order synchronous dataflow programs (GD, AG, MP), pp. 101–110.
ESOPESOP-2008-Ong #approach #semantics #verification
Verification of Higher-Order Computation: A Game-Semantic Approach (CHLO), pp. 299–306.
ESOPESOP-2008-PoswolskyS #dependent type #encoding #programming
Practical Programming with Higher-Order Encodings and Dependent Types (AP, CS), pp. 93–107.
FASEFASE-2008-BruckerW #named #ocl #proving #uml
HOL-OCL: A Formal Proof Environment for UML/OCL (ADB, BW), pp. 97–100.
FoSSaCSFoSSaCS-2008-GianantonioHL #λ-calculus
RPO, Second-Order Contexts, and λ-Calculus (PDG, FH, ML), pp. 334–349.
CSLCSL-2008-AbelR #type system
Syntactic Metatheory of Higher-Order Subtyping (AA, DR), pp. 446–460.
IJCARIJCAR-2008-BenzmullerPTF #automation #logic #named #proving #theorem proving
LEO-II — A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (CB, LCP, FT, AF), pp. 162–170.
IJCARIJCAR-2008-BenzmullerRS #logic #named
THF0 — The Core of the TPTP Language for Higher-Order Logic (CB, FR, GS), pp. 491–506.
LICSLICS-2008-CarayolHMOS #automaton #game studies
Winning Regions of Higher-Order Pushdown Games (AC, MH, AM, CHLO, OS), pp. 193–204.
LICSLICS-2008-Fiore #syntax
Second-Order and Dependently-Sorted Abstract Syntax (MPF), pp. 57–68.
LICSLICS-2008-LanesePSS #calculus #decidability #on the #process
On the Expressiveness and Decidability of Higher-Order Process Calculi (IL, JAP, DS, AS), pp. 145–155.
LICSLICS-2008-Pottier #anti
Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule (FP), pp. 331–340.
TAPTAP-2008-Cao #equivalence #finite #π-calculus
Equivalence Checking for a Finite Higher Order π-Calculus (ZC), pp. 30–47.
TLCATLCA-2007-LiptonN #constraints #logic programming #programming language #semantics
Higher-Order Logic Programming Languages with Constraints: A Semantics (JL, SN), pp. 272–289.
TLCATLCA-2007-MostrousY #mobile #process #type system
Two Session Typing Systems for Higher-Order Mobile Processes (DM, NY), pp. 321–335.
TLCATLCA-2007-Tatsuta #quantifier #set
Simple Saturated Sets for Disjunction and Second-Order Existential Quantification (MT), pp. 366–380.
ICFPICFP-2007-Park #type safety
Type-safe higher-order channels in ML-like languages (SP), pp. 191–202.
ICFPICFP-2007-Sereni #analysis #functional #graph #source code #termination
Termination analysis and call graph construction for higher-order functional programs (DS), pp. 71–84.
SPLCSPLC-2007-JanotaK #feature model #logic #modelling #reasoning
Reasoning about Feature Models in Higher-Order Logic (MJ, JRK), pp. 13–22.
SPLCSPLC-2007-OldevikH #product line
Higher-Order Transformations for Product Lines (JO, ØH), pp. 243–254.
OOPSLAOOPSLA-2007-ShanerLN #composition #source code #verification
Modular verification of higher-order methods with mandatory calls specified by model programs (SMS, GTL, DAN), pp. 351–368.
PADLPADL-2007-Liang #aspect-oriented #linear #logic #programming
Aspect-Oriented Programming in Higher-Order and Linear Logic (CCL), pp. 305–319.
POPLPOPL-2007-Might #analysis #source code
Logic-flow analysis of higher-order programs (MM), pp. 185–198.
POPLPOPL-2007-PearlmutterS #lazy evaluation #multi
Lazy multivariate higher-order forward-mode AD (BAP, JMS), pp. 155–160.
PPDPPPDP-2007-Hamana #data type #induction #semantics #type system
Higher-order semantic labelling for inductive datatype systems (MH), pp. 97–108.
DACDAC-2007-FengLZ #analysis #parametricity #performance #reduction #statistics #using
Fast Second-Order Statistical Static Timing Analysis Using Parameter Dimension Reduction (ZF, PL, YZ), pp. 244–249.
DACDAC-2007-YanTLM #named #reduction
SBPOR: Second-Order Balanced Truncation for Passive Order Reduction of RLC Circuits (BY, SXDT, PL, BM), pp. 158–161.
ESOPESOP-2007-LiOS #compilation #logic #set
Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic (GL, SO, KS), pp. 205–219.
ESOPESOP-2007-Pitts #equivalence
Techniques for Contextual Equivalence in Higher-Order, Typed Languages (AMP), p. 1.
FoSSaCSFoSSaCS-2007-HagueO #analysis #automaton
Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems (MH, CHLO), pp. 213–227.
FoSSaCSFoSSaCS-2007-YoshidaHB #logic #reasoning
Logical Reasoning for Higher-Order Functions with Local State (NY, KH, MB), pp. 361–377.
CADECADE-2007-LiS #compilation #logic
Compilation as Rewriting in Higher Order Logic (GL, KS), pp. 19–34.
LICSLICS-2007-SangiorgiKS #bisimulation
Environmental Bisimulations for Higher-Order Languages (DS, NK, ES), pp. 293–302.
LICSLICS-2007-Stirling #automaton #game studies
Higher-Order Matching, Games and Automata (CS), pp. 326–335.
TAPTAP-2007-BruckerW #generative #testing
Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing (ADB, BW), pp. 149–168.
ICALPICALP-v2-2006-HondaBY #logic
Descriptive and Relative Completeness of Logics for Higher-Order Functions (KH, MB, NY), pp. 360–371.
ICALPICALP-v2-2006-Stirling #approach #game studies
A Game-Theoretic Approach to Deciding Higher-Order Matching (CS), pp. 348–359.
RTARTA-2006-Bruggink #finite #product line #proving #using
A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property (HJSB), pp. 372–386.
RTARTA-2006-JouannaudR
Higher-Order Orderings for Normal Rewriting (JPJ, AR), pp. 387–399.
RTARTA-2006-Koprowski #recursion
Certified Higher-Order Recursive Path Ordering (AK), pp. 227–241.
RTARTA-2006-LevySV #bound #unification
Bounded Second-Order Unification Is NP-Complete (JL, MSS, MV), pp. 400–414.
RTARTA-2006-Obua #logic
Checking Conservativity of Overloaded Definitions in Higher-Order Logic (SO), pp. 212–226.
FLOPSFLOPS-2006-CasasCH #approach #evaluation #functional #lazy evaluation
A Syntactic Approach to Combining Functional Notation, Lazy Evaluation, and Higher-Order in LP Systems (AC, DC, MVH), pp. 146–162.
ICMLICML-2006-AgarwalBB #graph #learning
Higher order learning with graphs (SA, KB, SB), pp. 17–24.
ICMLICML-2006-McAuleyCSF #image #learning
Learning high-order MRF priors of color images (JJM, TSC, AJS, MOF), pp. 617–624.
ICPRICPR-v2-2006-HorvathJZK #detection
A Higher-Order Active Contour Model for Tree Detection (PH, IJ, JZ, ZK), pp. 130–133.
PEPMPEPM-2006-WangCK #aspect-oriented #functional #weaving
Type-directed weaving of aspects for higher-order functional languages (MW, KC, SCK), pp. 78–87.
POPLPOPL-2006-KoutavasW #bisimulation #imperative #reasoning #source code
Small bisimulations for reasoning about higher-order imperative programs (VK, MW), pp. 141–152.
DATEDATE-2006-MajidzadehS #design #novel
Arbitrary design of high order noise transfer function for a novel class of reduced-sample-rate sigma-delta-pipeline ADCs (VM, OS), pp. 138–143.
DATEDATE-2006-PanditKMP #hardware #synthesis
High level synthesis of higher order continuous time state variable filters with minimum sensitivity and hardware count (SP, SK, CAM, AP), pp. 1203–1204.
FoSSaCSFoSSaCS-2006-Cao #bisimulation #π-calculus
More on Bisimulations for Higher Order π-Calculus (ZC), pp. 63–78.
TACASTACAS-2006-GhicaM #composition #concurrent #source code
Compositional Model Extraction for Higher-Order Concurrent Programs (DRG, ASM), pp. 303–317.
CSLCSL-2006-HellaT #logic #problem
Complete Problems for Higher Order Logics (LH, JMTT), pp. 380–394.
CSLCSL-2006-ReusS #logic
Separation Logic for Higher-Order Store (BR, JS), pp. 575–590.
IJCARIJCAR-2006-GelderS #automation #generative #logic #parsing
Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation (AVG, GS), pp. 156–161.
IJCARIJCAR-2006-Krauss #logic #recursion
Partial Recursive Functions in Higher-Order Logic (AK), pp. 589–603.
IJCARIJCAR-2006-McLaughlin
An Interpretation of Isabelle/HOL in HOL Light (SM), pp. 192–204.
IJCARIJCAR-2006-ObuaS
Importing HOL into Isabelle/HOL (SO, SS), pp. 298–302.
IJCARIJCAR-2006-Pientka #approach #lightweight #unification
Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach (BP), pp. 362–376.
IJCARIJCAR-2006-UrbanB #combinator #data type #recursion
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL (CU, SB), pp. 498–512.
LICSLICS-2006-Ong #model checking #on the #recursion
On Model-Checking Trees Generated by Higher-Order Recursion Schemes (CHLO), pp. 81–90.
HTHT-2005-HorieYK #analysis #rank #web
Higher-order rank analysis for web structure (IH, KY, KK), pp. 98–106.
WCREWCRE-2005-SpoonS #navigation #scalability #semantics
Semantic Navigation of Large Code Bases in Higher-Order, Dynamically Typed Languages (SAS, OS), pp. 219–228.
ICALPICALP-2005-ReusS #hoare #logic
About Hoare Logics for Higher-Order Store (BR, TS), pp. 1337–1348.
RTARTA-2005-Hamana #algebra #termination
Universal Algebra for Termination of Higher-Order Rewriting (MH), pp. 135–149.
RTARTA-2005-Yoshinaka #linear #λ-calculus
Higher-Order Matching in the Linear λ Calculus in the Absence of Constants Is NP-Complete (RY), pp. 235–249.
SEFMSEFM-2005-BlechGG #verification
Formal Verification of Dead Code Elimination in Isabelle/HOL (JOB, LG, SG), pp. 200–209.
TLCATLCA-2005-AehligMO #decidability #monad #recursion
The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable (KA, JGdM, CHLO), pp. 39–54.
TLCATLCA-2005-BoveC #recursion
Recursive Functions with Higher Order Domains (AB, VC), pp. 116–130.
TLCATLCA-2005-SchurmannPS #calculus #encoding #functional #programming
The [triangle]-Calculus. Functional Programming with Higher-Order Encodings (CS, AP, JS), pp. 339–353.
TLCATLCA-2005-Zanardini
Higher-Order Abstract Non-interference (DZ), pp. 417–432.
ICFPICFP-2005-BergerHY #alias #analysis #imperative #logic
A logical analysis of aliasing in imperative higher-order functions (MB, KH, NY), pp. 280–293.
KDDKDD-2005-GaoLZCM #clustering #consistency #graph #semistructured data
Consistent bipartite graph co-partitioning for star-structured high-order heterogeneous data co-clustering (BG, TYL, XZ, QC, WYM), pp. 41–50.
PLDIPLDI-2005-KrishnaswamiA #encapsulation
Permission-based ownership: encapsulating state in higher-order typed languages (NRK, JA), pp. 96–106.
COCVCOCV-J-2005-BlechGLM #code generation #comparison #correctness #optimisation #proving
Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL (JOB, SG, JL, SM), pp. 33–51.
DATEDATE-2005-BhaduriV #induction #metric
Inductive and Capacitive Coupling Aware Routing Methodology Driven by a Higher Order RLCK Moment Metric (AB, RV), pp. 922–923.
ESOPESOP-2005-BieringBT #logic
BI Hyperdoctrines and Higher-Order Separation Logic (BB, LB, NTS), pp. 233–247.
FASEFASE-2005-HausmannMS #induction
Iterative Circular Coinduction for CoCasl in Isabelle/HOL (DH, TM, LS), pp. 341–356.
FoSSaCSFoSSaCS-2005-MurawskiW #algol #decidability
Third-Order Idealized Algol with Iteration Is Decidable (ASM, IW), pp. 202–218.
CADECADE-2005-Pientka #logic programming
Tabling for Higher-Order Logic Programming (BP), pp. 54–68.
CADECADE-2005-UrbanT
Nominal Techniques in Isabelle/HOL (CU, CT), pp. 38–53.
CSLCSL-2005-CourcelleD #composition #graph #logic #monad
The Modular Decomposition of Countable Graphs: Constructions in Monadic Second-Order Logic (BC, CD), pp. 325–338.
CSLCSL-2005-Stirling #game studies
Higher-Order Matching and Games (CS), pp. 119–134.
FATESFATES-2005-BruckerW #interactive #testing
Interactive Testing with HOL-TestGen (ADB, BW), pp. 87–102.
ICLPICLP-2005-NadathurL #on the fly #unification
Practical Higher-Order Pattern Unification with On-the-Fly Raising (GN, NL), pp. 371–386.
LICSLICS-2005-BirkedalTY #semantics #type system
Semantics of Separation-Logic Typing and Higher-Order Frame Rules (LB, NTS, HY), pp. 260–269.
LICSLICS-2005-HondaYB #imperative #logic
An Observationally Complete Program Logic for Imperative Higher-Order Frame Rules (KH, NY, MB), pp. 270–279.
LICSLICS-2005-Lago #geometry #linear #recursion
The Geometry of Linear Higher-Order Recursion (UDL), pp. 366–375.
PODSPODS-2004-FaginPKT #dependence
Composing Schema Mappings: Second-Order Dependencies to the Rescue (RF, PGK, LP, WCT), pp. 83–94.
RTARTA-2004-AotoYT #induction #theorem
Inductive Theorems for Higher-Order Rewriting (TA, TY, YT), pp. 269–284.
RTARTA-2004-Blanqui #term rewriting #termination #type system
A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems (FB), pp. 24–39.
RTARTA-2004-LevySV #monad #unification
Monadic Second-Order Unification Is NP-Complete (JL, MSS, MV), pp. 55–69.
RTARTA-2004-Toyama #lisp #term rewriting #termination
Termination of S-Expression Rewriting Systems: Lexicographic Path Ordering for Higher-Order Terms (YT), pp. 40–54.
SEFMSEFM-2004-BerghoferN #random testing #testing
Random Testing in Isabelle/HOL (SB, TN), pp. 230–239.
ICFPICFP-2004-GauthierP #canonical #first-order #matter #recursion
Numbering matters: first-order canonical forms for second-order recursive types (NG, FP), pp. 150–161.
ICFPICFP-2004-MarlowJ #performance
Making a fast curry: push/enter vs. eval/apply for higher-order languages (SM, SLPJ), pp. 4–15.
ICPRICPR-v2-2004-LindeL #recognition #using
Object Recognition Using Composed Receptive Field Histograms of Higher Dimensionality (OL, TL), pp. 1–6.
ICPRICPR-v4-2004-KobayashiO #identification #multi #polynomial #using
Action and Simultaneous Multiple-Person Identification Using Cubic Higher-Order Local Auto-Correlation (TK, NO), pp. 741–744.
POPLPOPL-2004-Yoshida #dependent type #mobile #process
Channel dependent types for higher-order mobile processes (NY), pp. 147–160.
PPDPPPDP-2004-HondaY #composition #logic #polymorphism
A compositional logic for polymorphic higher-order functions (KH, NY), pp. 191–202.
SACSAC-2004-BettiniBL #calculus #mixin
A core calculus of higher-order mixins and classes (LB, VB, SL), pp. 1508–1509.
DACDAC-2004-YangM #adaptation #modelling
An Essentially Non-Oscillatory (ENO) high-order accurate Adaptive table model for device modeling (BY, BM), pp. 864–867.
CSLCSL-2004-GrooteS #linear #λ-calculus
Higher-Order Matching in the Linear λ-calculus with Pairing (PdG, SS), pp. 220–234.
CSLCSL-2004-Skelley #bound
A Third-Order Bounded Arithmetic Theory for PSPACE (AS), pp. 340–354.
IJCARIJCAR-2004-AvigadD #formal method
Formalizing O Notation in Isabelle/HOL (JA, KD), pp. 357–371.
IJCARIJCAR-2004-Gottlob #finite #logic #research
Second-Order Logic over Finite Structures — Report on a Research Programme (GG), pp. 229–243.
LICSLICS-2004-CookK
A Second-Order Theory for NL (SAC, AK), pp. 398–407.
LICSLICS-2004-NguyenC
VTC circ: A Second-Order Theory for TCcirc (PN, SAC), pp. 378–387.
ICDARICDAR-2003-KangD #classification #dependence #multi
Combining Multiple Classifiers based on Third-Order Dependency (HJK, DSD), pp. 21–25.
ICALPICALP-2003-Cachat #automaton #game studies #graph
Higher Order Pushdown Automata, the Caucal Hierarchy of Graphs and Parity Games (TC), pp. 556–569.
ICALPICALP-2003-Hannay #axiom #data type
Axiomatic Criteria for Quotients and Subobjects for Higher-Order Data Types (JEH), pp. 903–917.
ICALPICALP-2003-KlaedtkeR #logic #monad
Monadic Second-Order Logics with Cardinalities (FK, HR), pp. 681–696.
RTARTA-2003-Bruggink
Residuals in Higher-Order Rewriting (HJSB), pp. 123–137.
RTARTA-2003-SalvatiG #complexity #linear #on the #λ-calculus
On the Complexity of Higher-Order Matching in the Linear λ-Calculus (SS, PdG), pp. 234–245.
TLCATLCA-2003-Power
A Universal Embedding for the Higher Order Structure of Computational Effects (JP), pp. 301–315.
ICFPICFP-2003-WashburnW #encoding #morphism #parametricity #polymorphism #syntax
Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism (GW, SW), pp. 249–262.
IFLIFL-2003-VasconcelosH #equation #functional #polymorphism #recursion #source code
Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs (PBV, KH), pp. 86–101.
ECOOPECOOP-2003-Ernst
Higher-Order Hierarchies (EE), pp. 303–328.
LOPSTRLOPSTR-2003-YokoyamaHT #program transformation
Deterministic Higher-Order Patterns for Program Transformation (TY, ZH, MT), pp. 128–142.
POPLPOPL-2003-DreyerCH #type system
A type system for higher-order modules (DD, KC, RH), pp. 236–249.
POPLPOPL-2003-SchmittS #calculus #distributed #process
The m-calculus: a higher-order distributed process calculus (AS, JBS), pp. 50–61.
ESOPESOP-2003-HaackW #fault #slicing
Type Error Slicing in Implicitly Typed Higher-Order Languages (CH, JBW), pp. 284–301.
ESOPESOP-2003-Nieto
The Rely-Guarantee Method in Isabelle/HOL (LPN), pp. 348–362.
FoSSaCSFoSSaCS-2003-AbelMU #data type
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes (AA, RM, TU), pp. 54–69.
FoSSaCSFoSSaCS-2003-Bonelli #calculus #normalisation
A Normalisation Result for Higher-Order Calculi with Explicit Substitutions (EB), pp. 153–168.
FoSSaCSFoSSaCS-2003-MomiglianoA #multi #syntax
Multi-level Meta-reasoning with Higher-Order Abstract Syntax (AM, SA), pp. 375–391.
STOCSTOC-2003-CoppersmithS #semistructured data
Reconstructing curves in three (and higher) dimensional space from noisy data (DC, MS), pp. 136–142.
CADECADE-2003-MehtaN #logic #pointer #proving #source code
Proving Pointer Programs in Higher-Order Logic (FM, TN), pp. 121–135.
CADECADE-2003-PientkaP #optimisation #unification
Optimizing Higher-Order Pattern Unification (BP, FP), pp. 473–487.
CADECADE-2003-Schmidt-Schauss #bound #decidability
Decidability of Arity-Bounded Higher-Order Matching (MSS), pp. 488–502.
ICLPICLP-2003-Pientka
Higher-Order Substitution Tree Indexing (BP), pp. 377–391.
LICSLICS-2003-GurevichS #monad
Spectra of Monadic Second-Order Formulas with One Unary Function (YG, SS), pp. 291–300.
RTARTA-2002-DoughertyW #decidability
A Decidable Variant of Higher Order Matching (DJD, TW), pp. 340–351.
RTARTA-2002-LevyV #problem #unification
Currying Second-Order Unification Problems (JL, MV), pp. 326–339.
FLOPSFLOPS-2002-KasuyaSA #normalisation #term rewriting
Descendants and Head Normalization of Higher-Order Rewrite Systems (HK, MS, KA), pp. 198–211.
ICFPICFP-2002-FindlerF #contract
Contracts for higher-order functions (RBF, MF), pp. 48–59.
ICFPICFP-2002-NeubauerT #morphism #polymorphism
Type classes with more higher-order polymorphism (MN, PT), pp. 179–190.
DiGRACGDC-2002-Kucklich #case study #game studies
The Study of Computer Games as a Second-Order Cybernetic System (JK).
ICPRICPR-v2-2002-ForestiCS #adaptation #pattern matching #pattern recognition #recognition
Adaptive High Order Neural Trees for Pattern Recognition (GLF, CM, LS), p. 877–?.
KRKR-2002-Gardenfors #concept #induction #similarity
The Role of Higher Order Similarity in Induction and Concept Formation (PG), p. 629.
UMLUML-2002-BruckerW #case study #design #experience #named #ocl
HOL-OCL: Experiences, Consequences and Design Choices (ADB, BW), pp. 196–211.
LOPSTRLOPSTR-2002-ColvinHHS #logic programming #refinement #source code
Refinement of Higher-Order Logic Programs (RC, IJH, DH, PAS), pp. 126–143.
LOPSTRLOPSTR-2002-FioravantiPP #logic #logic programming #monad #program transformation #source code
Combining Logic Programs and Monadic Second Order Logics by Program Transformation (FF, AP, MP), pp. 160–181.
PADLPADL-2002-Liang #compilation #logic programming
Compiler Construction in Higher Order Logic Programming (CL), pp. 47–63.
PEPMPEPM-2002-GomezL #analysis #automation #bound
Automatic time-bound analysis for a higher-order language (GG, YAL), pp. 75–86.
PPDPPPDP-2002-OstrovskyPT #calculus #towards
Towards a primitive higher order calculus of broadcasting systems (KO, KVSP, WT), pp. 2–13.
GPCEGPCE-2002-Saraiva #attribute grammar #component #programming
Component-Based Programming for Higher-Order Attribute Grammars (JS), pp. 268–282.
ESOPESOP-2002-Glew #formal method
A Theory of Second-Order Trees (NG), pp. 147–161.
ESOPESOP-2002-Weirich #analysis
Higher-Order Intensional Type Analysis (SW), pp. 98–114.
FoSSaCSFoSSaCS-2002-Courcelle #monad #semantics
Semantical Evaluations as Monadic Second-Order Compatible Structure Transformations (BC), pp. 1–4.
FoSSaCSFoSSaCS-2002-KnapikNU #automaton
Higher-Order Pushdown Trees Are Easy (TK, DN, PU), pp. 205–222.
CADECADE-2002-Brown #proving #set #theorem proving
Solving for Set Variables in Higher-Order Theorem Proving (CEB), pp. 408–422.
CSLCSL-2002-Goubault-Larrecq #constraints #set
Higher-Order Positive Set Constraints (JGL), pp. 473–489.
CSLCSL-2002-Schmidt-SchaussS #bound #decidability #unification
Decidability of Bounded Higher-Order Unification (MSS, KUS), pp. 522–536.
ICLPICLP-2002-Pientka #logic programming
A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming (BP), pp. 271–286.
LICSLICS-2002-FrickG #complexity #first-order #logic #monad #revisited
The Complexity of First-Order and Monadic Second-Order Logic Revisited (MF, MG), pp. 215–224.
VMCAIVMCAI-2002-CoppoD #mobile
A Fully Abstract Model for Higher-Order Mobile Ambients (MC, MDC), pp. 255–271.
DLTDLT-2001-EiterGS #logic #string
Second-Order Logic over Strings: Regular and Non-regular Fragments (TE, GG, TS), pp. 37–56.
RTARTA-2001-BerarducciB #algebra #recursion
General Recursion on Second Order Term Algebras (AB, CB), pp. 15–30.
RTARTA-2001-BonelliKR #first-order
From Higher-Order to First-Order Rewriting (EB, DK, AR), pp. 47–62.
RTARTA-2001-Raamsdonk #on the #termination
On Termination of Higher-Order Rewriting (FvR), pp. 261–275.
TLCATLCA-2001-Geuvers #dependent type #induction #type system
Induction Is Not Derivable in Second Order Dependent Type Theory (HG), pp. 166–181.
TLCATLCA-2001-Leiss #independence #representation
Second-Order Pre-Logical Relations and Representation Independence (HL), pp. 298–314.
TLCATLCA-2001-Matthes #induction #λ-calculus #μ-calculus
Parigot’s Second Order λμ-Calculus and Inductive Types (RM), pp. 329–343.
FLOPSFLOPS-2001-DanvyN
A Higher-Order Colon Translation (OD, LRN), pp. 78–91.
FLOPSFLOPS-2001-LeachN #constraints #logic programming #programming language
A Higher-Order Logic Programming Language with Constraints (JL, SN), pp. 108–122.
ASEASE-2001-CookIM #proving #synthesis #theorem proving
Higher Order Function Synthesis Through Proof Planning (AC, AI, GM), pp. 307–310.
FoSSaCSFoSSaCS-2001-RocklHB #formal method #induction #syntax #π-calculus
Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the π-Calculus and Mechanizing the Theory of Contexts (CR, DH, SB), pp. 364–378.
CSLCSL-2001-Bezem #logic programming #source code
An Improved Extensionality Criterion for Higher-Order Logic Programs (MB), pp. 203–216.
CSLCSL-2001-KorovinaK #semantics
Semantic Characterisations of Second-Order Computability over the Real Numbers (MVK, OVK), pp. 160–172.
CSLCSL-2001-Schurmann #encoding #recursion
Recursion for Higher-Order Encodings (CS), pp. 585–599.
IJCARIJCAR-2001-Beeson #proving #theorem proving
A Second-Order Theorem Prover Applied to Circumscription (MB), pp. 318–324.
IJCARIJCAR-2001-Pientka #logic programming #reduction #source code #termination
Termination and Reduction Checking for Higher-Order Logic Programs (BP), pp. 401–415.
LICSLICS-2001-CookK #reasoning #theorem #using
A Second-Order System for Polytime Reasoning Using Graedel’s Theorem (SAC, AK), pp. 177–186.
RTARTA-2000-Blanqui #confluence #term rewriting #termination
Termination and Confluence of Higher-Order Rewrite Systems (FB), pp. 47–61.
RTARTA-2000-BonelliKR
A de Bruijn Notation for Higher-Order Rewriting (EB, DK, AR), pp. 62–79.
RTARTA-2000-Groote #linear
Linear Higher-Order Matching Is NP-Complete (PdG), pp. 127–140.
RTARTA-2000-LevyV #constraints #linear #unification
Linear Second-Order Unification and Context Unification with Tree-Regular Constraints (JL, MV), pp. 156–171.
ICEISICEIS-2000-AldenbergHP
High-Order Effects of Groupware: A Case of Censequences of Lotus Notes (BA, MSHH, SCAP), pp. 377–384.
LOPSTRLOPSTR-2000-SeresS #logic programming #source code
Higher-order transformation of logic programs (SS, JMS).
LOPSTRLOPSTR-2000-VanhoofB #analysis #composition #towards
Towards a modular binding-time analysis for higher-order Mercury (WV, MB).
LOPSTRLOPSTR-J-2000-SeresS #logic programming #source code
Higher-Order Transformation of Logic Programs (SS, JMS), pp. 57–68.
FoSSaCSFoSSaCS-2000-Hannay #simulation #system f
A Higher-Order Simulation Relation for System F (JEH), pp. 130–145.
CADECADE-2000-AndrewsB #education #logic #named #proving #theorem proving #tutorial #using
Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic (PBA, CEB), pp. 511–512.
CADECADE-2000-MichaelA #bytecode #logic #semantics #syntax
Machine Instruction Syntax and Semantics in Higher Order Logic (NGM, AWA), pp. 7–24.
CAVCAV-2000-AyariB #bound #logic #monad
Bounded Model Construction for Monadic Second-Order Logics (AA, DAB), pp. 99–112.
ICLPCL-2000-LaceyRS #logic programming #synthesis
Logic Program Synthesis in a Higher-Order Setting (DL, JR, AS), pp. 87–100.
CSLCSL-2000-Naijun #calculus
Completeness of Higher-Order Duration Calculus (ZN), pp. 442–456.
ICALPICALP-1999-EngelfrietH #finite #logic #monad #transducer
Two-Way Finite State Transducers and Monadic Second-Order Logic (JE, HJH), pp. 311–320.
FMFM-v2-1999-JimenezO #algebra #framework
An Algebraic Framework for Higher-Order Modules (RMJ, FO), pp. 1778–1797.
RTARTA-1999-DowekHK #first-order #logic #named
HOL-λσ: An Intentional First-Order Expression of Higher-Order Logic (GD, TH, CK), pp. 317–331.
RTARTA-1999-Raamsdonk
Higher-Order Rewriting (FvR), pp. 220–239.
FLOPSFLOPS-1999-AntoyT
Typed Higher-Order Narrowing without Higher-Order Strategies (SA, APT), pp. 335–353.
FLOPSFLOPS-1999-MarinIS #lazy evaluation #on the
On Reducing the Search Space of Higher-Order Lazy Narrowing (MM, TI, TS), pp. 319–334.
FLOPSFLOPS-1999-MoorS #program transformation
Higher Order Matching for Program Transformation (OdM, GS), pp. 209–224.
ESOPESOP-1999-Thiemann
Higher-Order Code Splicing (PT), pp. 243–257.
FASEFASE-1999-NipkowN
Owicki/Gries in Isabelle/HOL (TN, LPN), pp. 188–203.
TACASTACAS-1999-Pusch #bytecode #java #proving #specification #verification
Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL (CP), pp. 89–103.
CADECADE-1999-Benzmuller
Extensional Higher-Order Paramodulation and RUE-Resolution (CB), pp. 399–413.
CADECADE-1999-Lopes #automation #generative #logic #proving
Automatic Generation of Proof Search Strategies for Second-order Logic (RHCL), pp. 414–428.
CADECADE-1999-Wierzbicki #complexity
Complexity of the higher order matching (TW), pp. 82–96.
CSLCSL-1999-CompagnoniG #symmetry #type system
Anti-Symmetry of Higher-Order Subtyping (ABC, HG), pp. 420–438.
ICLPICLP-1999-MomiglianoP #problem
The Relative Complement Problem for Higher-Order Patterns (AM, FP), pp. 380–394.
LICSLICS-1999-Hofmann #analysis #semantics #syntax
Semantical Analysis of Higher-Order Abstract Syntax (MH0), pp. 204–213.
LICSLICS-1999-JouannaudR #recursion
The Higher-Order Recursive Path Ordering (JPJ, AR), pp. 402–411.
HTHT-1998-Ricardo #hypermedia
Stalking the Paratext: Speculations on Hypertext Links as a Second Order Text (FJR), pp. 142–151.
PASTEPASTE-1998-WadellA #performance #source code #visualisation
Visualizing the Performance of Higher-Order Programs (OW, JMA), pp. 75–82.
ICALPICALP-1998-Walukiewicz98a #reduction
A Total AC-Compatible Reduction Ordering on Higher-Order Terms (DW), pp. 530–542.
FMFM-1998-Karlsen #framework #integration #tool support
The UniForM WorkBench — A Higher Order Tool Integration Framework (EWK), pp. 266–280.
FMFM-1998-Woodcock
The wHOLe System (MEW), pp. 359–366.
RTARTA-1998-DanvyR #partial evaluation
Higher-Order Rewriting and Partial Evaluation (OD, KHR), pp. 286–301.
RTARTA-1998-Levy #decidability #problem #unification
Decidable and Undecidable Second-Order Unification Problems (JL), pp. 47–60.
RTARTA-1998-MullerN #constraints #logic #monad
Ordering Constraints over Feature Trees Expressed in Second-Order Monadic Logic (MM, JN), pp. 196–210.
ICFPICFP-1998-HannanH
Higher-Order Arity Raising (JH, PH), pp. 27–38.
IFLIFL-1998-Pape
Higher Order Demand Propagation (DP), pp. 153–168.
KDDKDD-1998-SteegRW #correlation #detection #multi #performance
Coincidence Detection: A Fast Method for Discovering Higher-Order Correlations in Multidimensional Data (EWS, DAR, EW), pp. 112–120.
PPDPALP-PLILP-1998-Pitts #semantics
Operational Versus Denotational Methods in the Semantics of Higher Order Languages (AMP), pp. 282–283.
POPLPOPL-1998-HannanH
Higher-Order unCurrying (JH, PH), pp. 1–11.
POPLPOPL-1998-JagannathanTWW #alias #analysis
Single and Loving It: Must-Alias Analysis for Higher-Order Languages (SJ, PT, SW, AKW), pp. 329–341.
POPLPOPL-1998-Schubert #morphism #polymorphism #type inference #unification
Second-Order Unification and Type Inference for Church-Style Polymorphism (AS), pp. 279–288.
CADECADE-1998-BenzmullerK
Extensional Higher-Order Resolution (CB, MK), pp. 56–71.
CADECADE-1998-BenzmullerK98a #proving #theorem proving
System Description: LEO — A Higher-Order Theorem Prover (CB, MK), pp. 139–144.
CADECADE-1998-Pagano #calculus #first-order #reduction
X.R.S : Explicit Reduction Systems — A First-Order Calculus for Higher-Order Calculi (BP), pp. 72–87.
CADECADE-1998-RichardsonSG #logic #proving #theorem proving
System Description: Proof Planning in Higher-Order Logic with Lambda-Clam (JR, AS, IG), pp. 129–133.
LICSLICS-1998-Bars #logic
Fragments of Existential Second-Order Logic without 0-1 Laws (JMLB), pp. 525–536.
LICSLICS-1998-Bernstein #congruence #semantics #theorem
A Congruence Theorem for Structured Operational Semantics of Higher-Order Languages (KLB), pp. 153–164.
LICSLICS-1998-EiterGG #logic #string
Existential Second-Order Logic over Strings (TE, GG, YG), pp. 16–27.
LICSLICS-1998-HermidaMP #multi
Higher Dimensional Multigraphs (CH, MM, JP), pp. 199–206.
LICSLICS-1998-Veanes #unification
The Relation Between Second-Order Unification and Simultaneous Rigid E-Unification (MV), pp. 264–275.
ICALPICALP-1997-CosmoG #composition #on the #λ-calculus
On Modular Properties of Higher Order Extensional λ Calculi (RDC, NG), pp. 237–247.
FMFME-1997-TejW #csp
A Corrected Failure Divergence Model for CSP in Isabelle/HOL (HT, BW), pp. 318–337.
TLCATLCA-1997-DespeyrouxPS #recursion #syntax
Primitive Recursion for Higher-Order Abstract Syntax (JD, FP, CS), pp. 147–163.
ICFPICFP-1997-BlumeA #approach #named #optimisation
λ-Splitting: A Higher-Order Approach to Cross-Module Optimizations (MB, AWA), pp. 112–124.
ICFPICFP-1997-Crary #implementation #type system
Foundations for the Implementation of Higher-Order Subtyping (KC), pp. 125–135.
ICGTGG-Handbook-Vol1-Courcelle #graph transformation #logic #monad
The Expression of Graph Properties and Graph Transformations in Monadic Second-Order Logic (BC), pp. 313–400.
EDOCEDOC-1997-ClassenWH #adaptation #corba #towards #workflow
Towards evolutionary and adaptive workflow systems-infrastructure support based on Higher-Order Object Nets and CORBA (IC, HW, YH), p. 300–?.
PPDPALP-1997-KirchnerR #equation #unification
Higher-Order Equational Unification via Explicit Substitutions (CK, CR), pp. 61–75.
PPDPALP-1997-Steggles #algebra #specification
Parameterised Higher-Order Algebraic Specifications (LJS), pp. 76–98.
PPDPALP-1997-SuzukiNI #calculus #functional #lazy evaluation #logic
Higher-Order Lazy Narrowing Calculus: A Computation Model for a Higher-Order Functional Logic Language (TS, KN, TI), pp. 99–113.
LOPSTRLOPSTR-1997-NaishS #re-engineering
A Higher Order Reconstruction of Stepwise Enhancement (LN, LS), pp. 245–262.
PLDIPLDI-1997-JensenJKS #automation #logic #monad #pointer #source code #using #verification
Automatic Verification of Pointer Programs using Monadic Second-Order Logic (JLJ, MEJ, NK, MIS), pp. 226–236.
PPDPPLILP-1997-Mossin #graph
Higher-Order Value Flow Graphs (CM), pp. 159–173.
POPLPOPL-1997-BourdoncleM #multi #polymorphism
Type-Checking Higher-Order Polymorphic Multi-Methods (FB, SM), pp. 302–315.
POPLPOPL-1997-SeidlS #constraints #deforestation
Constraints to Stop Higher-Order Deforestation (HS, MHS), pp. 400–413.
SASSAS-1997-PanitzS #automation #functional #named #proving #source code #strict #termination
TEA: Automatically Proving Termination of Programs in a Non-strict Higher-Order Functional Language (SEP, MSS), pp. 345–360.
TACASTACAS-1997-KelbMMG #flexibility #logic #monad #named #tool support
MOSEL: A FLexible Toolset for Monadic Second-Order Logic (PK, TMS, MM, CG), pp. 183–202.
TAPSOFTTAPSOFT-1997-BaldamusD #bisimulation #process
Modal Characterization of Weak Bisimulation for Higher-order Processes (Extended Abstract) (MB, JD), pp. 285–296.
TAPSOFTTAPSOFT-1997-MullerN
Traces of I/O-Automata in Isabelle/HOLCF (OM, TN), pp. 580–594.
TAPSOFTTAPSOFT-1997-Schubert #linear #problem
Linear Interpolation for the Higher-Order Matching Problem (AS), pp. 441–452.
CADECADE-1997-Hickey #framework #implementation #logic #named
Nuprl-Light: An Implementation Framework for Higher-Order Logics (JJH), pp. 395–399.
CSLCSL-1997-ComonJ #automaton
Higher-Order Matching and Tree Automata (HC, YJ), pp. 157–176.
CSLCSL-1997-HartonasH #concurrent #functional
Full Abstractness for a Functional/Concurrent Language with Higher-Order Value-Passing (CH, MH), pp. 239–254.
CSLCSL-1997-Schiering #approach #graph #logic #monad
A Hierarchical Approach to Monadic Second-Order Logic over Graphs (IS), pp. 424–440.
CSLCSL-1997-Schwentick #logic #power of
Padding and the Expressive Power of Existential Second-Order Logics (TS), pp. 461–477.
CSLCSL-1997-Staiger #monad
Rich ω-Words and Monadic Second-Order Arithmetic (LS), pp. 478–490.
ICLPICLP-1997-Gonzalez-MorenoHR #functional #logic programming
A Higher Order Rewriting Logic for Functional Logic Programming (JCGM, MTHG, MRA), pp. 153–167.
LICSLICS-1997-CervesatoP #linear
Linear Higher-Order Pre-Unification (IC, FP), pp. 422–433.
LICSLICS-1997-Goubault-Larrecq #unification
Ramified Higher-Order Unification (JGL), pp. 410–421.
LICSLICS-1997-McDowellM #logic #reasoning #syntax
A Logic for Reasoning with Higher-Order Abstract Syntax (RM, DM), pp. 434–445.
RTARTA-1996-CurienQS #performance
Efficient Second-Order Matching (RC, ZQ, HS), pp. 317–331.
RTARTA-1996-FettigL #finite #unification #λ-calculus
Unification of Higher-Order patterns in a Simply Typed λ-Calculus with Finite Products and terminal Type (RF, BL), pp. 347–361.
RTARTA-1996-HanusP
Higher-Order Narrowing with Definitional Trees (MH, CP), pp. 138–152.
RTARTA-1996-JouannaudR #normalisation #recursion
A Recursive Path Ordering for Higher-Order Terms in η-Long β-Normal Form (JPJ, AR), pp. 108–122.
RTARTA-1996-Levy #linear #unification
Linear Second-Order Unification (JL), pp. 332–346.
RTARTA-1996-Oostrom #product line
Higher-Order Families (VvO), pp. 392–407.
RTARTA-1996-Virga #dependent type
Higher-Order Superposition for Dependent Types (RV), pp. 123–137.
IFLIFL-1996-DebbabiFT #algorithm #analysis #concurrent #control flow #source code #type system
A Type-Based Algorithm for the Control-Flow Analysis of Higher-Order Concurrent Programs (MD, AF, NT), pp. 247–266.
ICPRICPR-1996-Horikawa #correlation #pattern matching #pattern recognition #recognition #similarity
Pattern recognition with invariance to similarity transformations based on the third-order correlation (YH), pp. 200–204.
ICPRICPR-1996-YuCXY #3d #approximate
3D shape and motion by SVD under higher-order approximation of perspective projection (HY, QC, GX, MY), pp. 456–460.
PPDPALP-1996-ManoO #normalisation #term rewriting
Unique Normal Form Property of Higher-Order Rewriting Systems (KM, MO), pp. 269–283.
PPDPPLILP-1996-Hamilton #deforestation
Higher Order Deforestation (GWH), pp. 213–227.
POPLPOPL-1996-Ashley #analysis #flexibility
A Practical and Flexible Flow Analysis for Higher-Order Languages (JMA), pp. 184–194.
SASSAS-1996-AndersenH #analysis #functional #partial evaluation #termination
Termination Analysis for Offline Partial Evaluation of a Higher Order Functional Language (PHA, CKH), pp. 67–82.
SACSAC-1996-SperberGT
Bootstrapping higher-order program transformers from interpreters (MS, RG, PT), pp. 408–413.
CCCC-1996-GeserKLRS #fixpoint
Non-monotone Fixpoint Iterations to Resolve Second Order Effects (AG, JK, GL, OR, BS), pp. 106–120.
TAPSOFTTAPSOFT-J-1995-HofmannS96 #abstraction #behaviour #logic #on the
On Behavioural Abstraction and Behavioural Satisfaction in Higher-Order Logic (MH, DS), pp. 3–45.
ESOPESOP-1996-RohwedderP #logic programming #source code #termination
Mode and Termination Checking for Higher-Order Logic Programs (ER, FP), pp. 296–310.
CADECADE-1996-Nipkow #proving
More Church-Rosser Proofs (in Isabelle/HOL) (TN), pp. 733–747.
CSLCSL-1996-Geuvers #dependent type #logic #modelling #type system
Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory (HG), pp. 167–181.
ICLPJICSLP-1996-DowekHKP #unification
Unification via Explicit Substitutions: The Case of Higher-Order Patterns (GD, TH, CK, FP), pp. 259–273.
LICSLICS-1996-CattaniS
Higher Dimensional Transition Systems (GLC, VS), pp. 55–62.
LICSLICS-1996-TiurynU #decidability #problem #type system
The Subtyping Problem for Second-Order Types is Undecidable (JT, PU), pp. 74–85.
RTARTA-1995-Boulton #semantics #strict
A Restricted Form on Higher-Order Rewriting Applied to an HDL Semantics (RJB), pp. 309–323.
RTARTA-1995-LysneP #term rewriting #termination
A Termination Ordering for Higher Order Rewrite System (OL, JP), pp. 26–40.
RTARTA-1995-Nipkow #term rewriting
Higher-Order Rewrite Systems (TN), p. 256.
TLCATLCA-1995-DespeyrouxFH #coq #syntax
Higher-Order Abstract Syntax in Coq (JD, APF, AH), pp. 124–138.
TLCATLCA-1995-Springintveld
Third-Order Matching in the Presence of Type Constructors (JS), pp. 428–442.
AFPAFP-1995-Jones95 #functional #morphism #polymorphism #programming
Functional Programming with Overloading and Higher-Order Polymorphism (MPJ), pp. 97–136.
PEPMPEPM-1995-Goubault #automaton #interpreter
Schedulers as Abstract Interpreter of Higher Dimensional Automata (EG), pp. 134–145.
PEPMPEPM-1995-MalmkjaerO
Polyvariant Specialisation for Higher-Order, Block-Structured Languages (KM, ), pp. 66–76.
PEPMPEPM-1995-Sands
Higher Order Expression Procedures (DS), pp. 178–189.
PLDIPLDI-1995-AikenFL #analysis #memory management
Better Static Memory Management: Improving Region-Based Analysis of Higher-Order Languages (AA, MF, RL), pp. 174–185.
PPDPPLILP-1995-NakaharaMI #calculus #functional #logic programming
A Complete Narrowing Calculus for Higher-Order Functional Logic Programming (KN, AM, TI), pp. 97–114.
POPLPOPL-1995-Biswas
Higher-Order Functors with Transparent Signatures (SKB), pp. 154–163.
POPLPOPL-1995-JagannathanW #analysis
A Unified Treatment of Flow Analysis in Higher-Order Languages (SJ, SW), pp. 393–407.
POPLPOPL-1995-Leroy
Applicative Functors and Fully Transparent Higher-Order Modules (XL), pp. 142–153.
POPLPOPL-1995-SansomJ #functional #profiling #strict
Time and Space Profiling for Non-Strict Higher-Order Functional Languages (PMS, SLPJ), pp. 355–366.
SASSAS-1995-Mohnen #analysis #inheritance #performance
Efficient Closure Utilisation by Higher-Order Inheritance Analysis (MM), pp. 261–278.
SASSAS-1995-Tofte #functional
Region Inference for Higher-Order Functional Languages (MT), pp. 19–20.
ESOPESOP-J-1994-AbadiC95 #formal method
A Theory of Primitive Objects: Second-Order Systems (MA, LC), pp. 81–116.
TACASTACAS-1995-HenriksenJJKPRS #logic #monad #named
Mona: Monadic Second-Order Logic in Practice (JGH, JLJ, MEJ, NK, RP, TR, AS), pp. 89–110.
TAPSOFTTAPSOFT-1995-AmadioD #process #reasoning
Reasoning about Higher-Order Processes (RMA, MD), pp. 202–216.
TAPSOFTTAPSOFT-1995-HofmannS #abstraction #behaviour #logic #on the
On Behavioral Abstraction and Behavioural Satisfaction in Higher-Order Logic (MH0, DS), pp. 247–261.
TAPSOFTTAPSOFT-1995-NielsonN #concurrent
Static and Dynamic Processor Allocation for Higher-Order Concurrent Languages (HRN, FN), pp. 590–604.
CAVCAV-1995-BasinK #hardware #logic #monad #using #verification
Hardware Verification using Monadic Second-Order Logic (DAB, NK), pp. 31–41.
ICLPICLP-1995-NilssonH #logic programming #source code
Constructing Logic Programs with Higher-Order Predicates (JFN, AH), p. 827.
ICLPILPS-1995-KuchenA
Higher Order Babel (HK, JA), p. 633.
ICLPILPS-1995-Prehofer #call-by #functional #logic programming
A Call-by-Need Strategy for Higher-Order Functional-Logic Programming (CP), pp. 147–161.
LICSLICS-1995-Comon #automaton #logic #monad
Sequentiality, Second Order Monadic Logic and Tree Automata (HC), pp. 508–517.
LICSLICS-1995-DowekHK #unification
Higher-Order Unification via Explicit Substitutions (GD, TH, CK), pp. 366–374.
LICSLICS-1995-LincolnSS #linear #logic #problem
Decision Problems for Second-Order Linear Logic (PL, AS, NS), pp. 476–485.
ICALPICALP-1994-Hennessy #modelling #process
Higher-Order Process and Their Models (MH), pp. 286–303.
LISPLFP-1994-KfouryW #algorithm #type inference #λ-calculus
A Direct Algorithm for Type Inference in the Rank-2 Fragment of the Second-Order λ-Calculus (AJK, JBW), pp. 196–207.
LISPLFP-1994-StefanescuZ #analysis #equation #framework #functional #source code
An Equational Framework for the Flow Analysis of Higher Order Functional Programs (DCS, YZ), pp. 318–327.
ICGTTAGT-1994-Courcelle #composition #graph #logic #monad
The Definition in Monadic Second-Order Logic of Modular Decompositions of Ordered Graphs (BC), pp. 487–501.
PPDPALP-1994-JonesR #functional #graph
Higher-Order Minimal Functional Graphs (NDJ, MR), pp. 242–252.
PEPMPEPM-1994-Baker-Finch #static analysis #type system
Type Theory and Projections for Higher-Order Static Analysis (CABF), pp. 43–52.
PEPMPEPM-1994-Thiemann
Higher-Order Redundancy Elimination (PT), pp. 73–83.
PPDPPLILP-1994-Serrano #analysis #compilation #control flow #functional #using
Using Higher-Order Control Flow Analysis When Compiling Functional Languages (MS), pp. 447–448.
POPLPOPL-1994-Bloom #communication #named #λ-calculus
CHOCOLATE: Calculi of Higher Order COmmunication and LAmbda TErms (BB), pp. 339–347.
POPLPOPL-1994-HarperL #approach
A Type-Theoretic Approach to Higher-Order Modules with Sharing (RH, ML), pp. 123–137.
POPLPOPL-1994-NielsonN #communication #concurrent #finite #source code
Higher-Order Concurrent Programs with Finite Communication Topology (HRN, FN), pp. 84–97.
POPLPOPL-1994-Qian #equation #logic programming
Higher-Order Equational Logic Programming (ZQ), pp. 254–267.
SACSAC-1994-RondogiannisW #data flow #hardware #implementation
Higher-order dataflow and its implementation on stock hardware (PR, WWW), pp. 431–435.
ESOPESOP-1994-Boerio #polymorphism #λ-calculus
Extending Pruning Techniques to Polymorphic Second order λ-Calculus (LB), pp. 120–134.
ESOPESOP-1994-MacQueenT #semantics
A Semantics for Higher-Order Functors (DBM, MT), pp. 409–423.
CADECADE-1994-MullerW #composition #theory and practice
Theory and Practice of Minimal Modular Higher-Order E-Unification (OM, FW), pp. 650–664.
CADECADE-1994-Prehofer #decidability #problem #unification
Decidable Higher-Order Unification Problems (CP), pp. 635–649.
ICLPICLP-1994-CairesM #logic programming #polymorphism #unification
Higher-Order Polymorphic Unification for Logic Programming (LC, LM), pp. 419–433.
ICLPICLP-1994-Reddy #aspect-oriented #logic programming
Higher-order Aspects of Logic Programming (USR), pp. 402–418.
ICLPILPS-1994-SchulteS #concurrent #constraints #encapsulation #programming
Encapsulated Search for Higher-order Concurrent Constraint Programming (CS, GS), pp. 505–520.
LICSLICS-1994-ColsonE #on the
On Strong Stability and Higher-Order Sequentiality (LC, TE), pp. 103–108.
LICSLICS-1994-Prehofer
Higher-Order Narrowing (CP), pp. 507–516.
LICSLICS-1994-Wells #decidability #λ-calculus
Typability and Type-Checking in the Second-Order λ-Calculus are Equivalent and Undecidable (JBW), pp. 176–185.
ICDARICDAR-1993-ChhabraABCLSSW #geometry #recognition #statistics
High-order statistically derived combinations of geometric features for handprinted character recognition (AKC, ZA, DB, GC, KL, PS, RS, BW), pp. 397–401.
SIGMODSIGMOD-1993-Guting #modelling #optimisation #query #specification
Second-Order Signature: A Tool for Specifying Data Models, Query Processing, and Optimization (RHG), pp. 277–286.
ICALPICALP-1993-KannegantiC #programming language #question #what
What is a Universal Higher-Order Programming Language? (RK, RC), pp. 682–695.
RTARTA-1993-GuiO #algebra #named #specification
LAMBDALG: Higher Order Algebraic Specification Language (YG, MO), pp. 462–466.
TLCATLCA-1993-BarbaneraF #term rewriting
Combining First and Higher Order Rewrite Systems with Type Assignment Systems (FB, MF), pp. 60–74.
TLCATLCA-1993-JacobsM #dependent type #logic #type system
Translating Dependent Type Theory into Higher Order Logic (BJ, TFM), pp. 209–229.
TLCATLCA-1993-Nipkow #confluence #orthogonal #term rewriting
Orthogonal Higher-Order Rewrite Systems are Confluent (TN), pp. 306–317.
FPCAFPCA-1993-Jones #morphism #polymorphism
A System of Constructor Classes: Overloading and Implicit Higher-Order Polymorphism (MPJ), pp. 52–64.
ECOOPECOOP-1993-CaseauP #object-oriented
Attaching Second-Order Types to Methods in an Object-Oriented Language (YC, LP), pp. 142–160.
PEPMPEPM-1993-Consel93a #partial evaluation
A Tour of Schism: A Partial Evaluation System For Higher-Order Applicative Languages (CC), pp. 145–154.
PEPMPEPM-1993-Davis #analysis
Higher-order Binding-time Analysis (KD), pp. 78–87.
PLDIPLDI-1993-Bourdoncle #debugging #imperative
Abstract Debugging of Higher-Order Imperative Languages (FB), pp. 46–55.
PPDPPLILP-1993-Rosendahl #sequence
Higher-Order Chaotic Iteration Sequences (MR), pp. 332–345.
TAPSOFTTAPSOFT-1993-Qian #linear #unification
Linear Unification of Higher-Order Patterns (ZQ), pp. 391–405.
TAPSOFTTAPSOFT-1993-Sangiorgi #π-calculus
From pi-Calculus to Higher-Order pi-Calculus - and Back (DS), pp. 151–166.
CSLCSL-1993-Milner #calculus
Higher-Order Action Calculi (RM), pp. 238–260.
ICLPICLP-1993-McCarty #induction #logic #prolog #proving #source code
Proving Inductive Properties of Prolog Programs in Second-Order Intuitionistic Logic (LTM), pp. 44–63.
ICLPILPS-1993-Felty #definite clause grammar #parsing #syntax
Definite Clause Grammars for Parsing Higher-Order Syntax (APF), p. 668.
KRKR-1992-GabbayO #logic #quantifier
Quantifier Elimination in Second-Order Predicate Logic (DMG, HJO), pp. 425–435.
ICMLML-1992-FengM #induction #logic #towards
Towards Inductive Generalization in Higher Order Logic (CF, SM), pp. 154–162.
ICMLML-1992-OmlinG #network #using
Training Second-Order Recurrent Neural Networks using Hints (CWO, CLG), pp. 361–366.
PEPMPEPM-1992-Chin #lazy evaluation
Fully Lazy Higher-Order Removal (WNC), pp. 38–47.
PEPMPEPM-1992-RufW #analysis #control flow #using
Improving the Accuracy of Higher-Order Specialization using Control Flow Analysis (ER, DW), pp. 67–74.
PPDPPLILP-1992-Hoa #bottom-up #interpreter #logic programming #programming language
A Bottom-Up Interpreter for a Higher-Order Logic Programming Language (AHBH), pp. 326–340.
PPDPPLILP-1992-Reus #algebra #implementation #specification
Implementing Higher-Order Functions in an Algebraic Specification Language with Narrowing (BR), pp. 483–484.
POPLPOPL-1992-BruceM #modelling #morphism #polymorphism #recursion #type system
PER Models of Subtyping, Recursive Types and Higher-Order Polymorphism (KBB, JCM), pp. 316–327.
POPLPOPL-1992-JagadeesanP #functional #logic #semantics
Abstract Semantics for a Higher-Order Functional Language with Logic Variables (RJ, KP), pp. 355–366.
POPLPOPL-1992-Tofte
Principal Signatures for Higher-Order Program Modules (MT), pp. 189–199.
CADECADE-1992-DoughertyJ #approach #combinator #logic
A Combinatory Logic Approach to Higher-order E-unification (DJD, PJ), pp. 79–93.
CSLCSL-1992-Gavilanes-FrancoLR #reasoning
Reasoning with Higher Order Partial Functions (AGF, FLC, MRA), pp. 167–181.
CSLCSL-1992-Tyszkiewicz #monad #on the
On Asymptotic Probabilities of Monadic Second Order Properties (JT), pp. 425–439.
ICLPJICSLP-1992-QianW
Higher-Order E-Unification for Arbitrary Theories (ZQ, KW), pp. 52–66.
LICSLICS-1992-Dowek #decidability
Third Order Matching is Decidable (GD), pp. 2–10.
RTARTA-1991-NipkowQ #composition
Modular Higher-Order E-Unification (TN, ZQ), pp. 200–214.
RTARTA-1991-Wolfram #equation #unification
Rewriting, and Equational Unification: the Higher-Order Cases (DAW), pp. 25–36.
FPCAFPCA-1991-Henglein #analysis #performance #type inference
Efficient Type Inference for Higher-Order Binding-Time Analysis (FH), pp. 448–472.
ICMLML-1991-KowalczykFG #network
Discovering Production Rules with Higher Order Neural Networks (AK, HLF, KG), pp. 158–162.
PLDIPLDI-1991-Reppy #concurrent #named
CML: A Higher-Order Concurrent Language (JHR), pp. 293–305.
PPDPPLILP-1991-ChenW #abstraction #compilation #logic programming
Compilation of Predicate Abstractions in Higher-Order Logic Programming (WC, DSW), pp. 287–298.
PPDPPLILP-1991-VogtSK #attribute grammar #incremental #performance
Efficient Incremental Evaluation of Higher order Attribute Grammars (HV, SDS, MFK), pp. 231–242.
POPLPOPL-1991-AbramskyJ #analysis #approach #polymorphism #relational #strict
A Relational Approach to Strictness Analysis for Higher-Order Polymorphic Functions (SA, TPJ), pp. 49–54.
POPLPOPL-1991-HengleinM #complexity #type inference #λ-calculus
The Complexity of Type Inference for Higher-Order Typed λ Calculi (FH, HGM), pp. 119–130.
SASWSA-1991-CousotC #abstract interpretation #functional #relational #source code
Relational Abstract Interpretation of Higher Order Functional Programs (PC, RC), pp. 33–36.
ESOPESOP-J-1990-Bondorf91 #automation #equation #recursion
Automatic Autoprojection of Higher Order Recursive Equations (AB), pp. 3–34.
TAPSOFTCCPSD-1991-Cardell-Oliver #logic #modelling #protocol #realtime #using
Using Higher Order Logic for Modelling Real-Time Protocols (RCO), pp. 259–282.
TAPSOFTCCPSD-1991-Krieg-BrucknerS #dependent type #in the large #in the small #inheritance #specification
Structuring Specifications in-the-Large and in-the-Small: Higher-Order Functions, Dependent Types and Inheritance in SPECTRAL (BKB, DS), pp. 313–336.
CAVCAV-1991-Nesi #induction #logic #process #proving #specification
Mechanizing a Proof by Induction of Process Algebrs Specifications in Higher Order Logic (MN), pp. 288–298.
ICLPICLP-1991-Hagiya #proving #theorem proving #unification
Higher-Order Unification as a Theorem Proving Procedure (MH), pp. 270–284.
ICLPISLP-1991-Wadge #logic programming
Higher-Order Horn Logic Programming (WWW), pp. 289–303.
LICSLICS-1991-JouannaudO #algebra #execution #specification
A Computation Model for Executable Higher-Order Algebraic Specification Languages (JPJ, MO), pp. 350–361.
LICSLICS-1991-Nipkow
Higher-Order Critical Pairs (TN), pp. 342–349.
LICSLICS-1991-PacholskiS #on the #similarity
On the 0-1 Law for the class of Existential Second Order Minimal Gödel Sentences with Equality (LP, WS), pp. 280–285.
ICALPICALP-1990-JagadeesanP #calculus #formal method #process
A Domain-Theoretic Model for a Higher-Order Process Calculus (RJ, PP), pp. 181–194.
LISPLFP-1990-Consel #analysis #functional
Binding Time Analysis for High Order Untyped Functional Languages (CC), pp. 264–272.
ICGTGG-1990-Engelfriet #graph #logic #monad
A Characterization of Context-Free NCE Graph Languages by Monadic Second-Order Logic on Trees (JE), pp. 311–327.
PPDPALP-1990-Qian #algebra
Higher-Order Order-Sorted Algebras (ZQ), pp. 86–100.
PLDIPLDI-1990-TeitelbaumC #attribute grammar #editing
Higher-Order Attribute Grammars and Editing Environments (TT, RC), pp. 197–208.
PPDPPLILP-1990-Queinnec #compilation #lisp
Compilation of Non-Linear, Second Order Patterns on S-Expressions (CQ), pp. 340–357.
POPLPOPL-1990-Deutsch #alias #functional #on the #specification
On Determining Lifetime and Aliasing of Dynamically Allocated Data in Higher-Order Functional Specifications (AD), pp. 157–168.
POPLPOPL-1990-HarperMM
Higher-Order Modules and the Phase Distinction (RH, JCM, EM), pp. 341–354.
ESOPESOP-1990-Bondorf #automation #equation #recursion
Automatic Autoprojection of Higher Order Recursive Equations (AB), pp. 70–87.
ESOPESOP-1990-GoldbergP #analysis #functional #implementation #optimisation #stack
Higher Order Escape Analysis: Optimizing Stack Allocation in Functional Program Implementations (BG, YGP), pp. 152–160.
ESOPESOP-1990-Sands #analysis #complexity #lazy evaluation
Complexity Analysis for a Lazy Higher-Order Language (DS), pp. 361–376.
CADECADE-1990-Hagiya #programming #proving #unification #using
Programming by Example and Proving by Example Using Higher-order Unification (MH), pp. 588–602.
CADECADE-1990-Snyder
Higher Order E-Unification (WS), pp. 573–587.
CAVCAV-1990-LoewensteinD #logic #multi #protocol #simulation #using #verification
Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic (PL, DLD), pp. 302–311.
ICLPCLP-1990-Miller90 #logic programming
Higher-Order Logic Programming (DM), p. 784.
ICLPCLP-1990-Sheng90 #logic programming #relational
HIFUNLOG : Logic Programming with Higher-order Relational Functions (YHS), pp. 529–545.
CSLCSL-1990-ArnborgPS #automaton #logic #monad
Monadic Second Order Logic, Tree Automata and Forbidden Minors (SA, AP, DS), pp. 1–16.
LICSLICS-1990-Courcelle #graph #monad #on the #set
On the Expression of Monadic Second-Order Graph Properties Without Quantifications Over Sets of Edges (BC), pp. 190–196.
SIGMODSIGMOD-1989-KiferL #inheritance #named #reasoning
F-Logic: A Higher-Order language for Reasoning about Objects, Inheritance, and Scheme (MK, GL), pp. 134–146.
ICALPICALP-1989-Courcelle #equation #graph #logic #monad
The Definability of Equational Graphs in Monadic Second-Order Logic (BC), pp. 207–221.
RTARTA-1989-Elliott #unification
Higher-order Unification with Dependent Function Types (CE), pp. 121–136.
FPCAFPCA-1989-NielsonN
Transformations on Higher-Order Functions (HRN, FN), pp. 129–143.
ICMLML-1989-DietzenP #framework #logic
Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization (SD, FP), pp. 447–449.
PLDIPLDI-1989-VogtSK #attribute grammar
Higher-Order Attribute Grammars (HV, SDS, MFK), pp. 131–145.
POPLPOPL-1989-Thomsen #calculus #communication
A Calculus of Higher Order Communicating Systems (BT), pp. 143–154.
TAPSOFTCAAP-1989-AstesianoC #modelling #on the #specification
On the Existence of Initial Models for Partial (Higher-Order) Conditional Specifications (EA, MC), pp. 74–88.
TAPSOFTCCIPL-1989-Mogensen #analysis
Binding Time Analysis for Polymorphically Typed Higher Order Languages (TÆM), pp. 298–312.
ICLPNACLP-1989-ChenKW #first-order #logic programming #named #semantics
HiLog: A First-Order Semantics for Higher-Order Logic Programming Constructs (WC, MK, DSW), pp. 1090–1114.
LISPLFP-1988-Pfenning #polymorphism #type inference #unification
Partial Polymorphic Type Inference and Higher-Order Unification (FP), pp. 153–163.
PLDIPLDI-1988-PfenningE #syntax
Higher-Order Abstract Syntax (FP, CE), pp. 199–208.
PLDIBest-of-PLDI-1988-Shivers88a #analysis #control flow #lessons learnt
Higher-order control-flow analysis in retrospect: lessons learned, lessons abandoned (with retrospective) (OS), pp. 257–269.
ESOPESOP-1988-Parigot #programming #proving #type system
Programming with Proofs: A Second Order Type Theory (MP), pp. 145–159.
CADECADE-1988-DonatW #learning #using
Learning and Applying Generalised Solutions using Higher Order Resolution (MRD, LAW), pp. 41–60.
CADECADE-1988-FeltyM #logic programming #programming language #proving #specification #theorem proving
Specifying Theorem Provers in a Higher-Order Logic Programming Language (APF, DM), pp. 61–80.
ICLPJICSCP-1988-HannanM88 #implementation #unification
Uses of Higher-Order Unification for Implementing Program Transformers (JH, DM), pp. 942–959.
LICSLICS-1988-Amadio #fixpoint #modelling #λ-calculus
A fixed point extension of the second order λ-calculus: observable equivalences and models (RMA), pp. 51–60.
LICSLICS-1988-Breazu-Tannen88a #algebra
Combining Algebra and Higher-Order Types (VT), pp. 82–90.
LICSLICS-1988-KolaitisV #logic #problem
0-1 Laws and Decision Problems for Fragments of Second-Order Logic (PGK, MYV), pp. 2–11.
PLDIPLDI-1987-Danvy #memory management
Memory allocation and higher-order functions (OD), pp. 241–252.
POPLPOPL-1987-FelleisenF #calculus
A Calculus for Assignments in Higher-Order Languages (MF, DPF), pp. 314–325.
TAPSOFTCFLP-1987-PettorossiS
Higher Order Generalization in Program Derivation (AP, AS), pp. 182–196.
STOCSTOC-1987-KolaitisV #problem
The Decision Problem for the Probabilities of Higher-Order Properties (PGK, MYV), pp. 425–435.
LICSLICS-1987-Mendler #constraints #recursion #λ-calculus
Recursive Types and Type Constraints in Second-Order λ Calculus (NPM), pp. 30–36.
ICLPSLP-1987-Chen87 #formal method #logic
A Theory of Modules Based on Second-Order Logic (WC), pp. 24–33.
LISPLFP-1986-BoehmCRO #case study #programming
Exact Real Arithmetic: A Case Study in Higher Order Programming (HJB, RC, MR, MJO), pp. 162–173.
ICGTGG-1986-Courcelle86a #graph #monad #on the #set
On context-free sets of graphs and their monadic second-order theory (BC), pp. 133–146.
POPLPOPL-1986-HudakY #analysis #strict #λ-calculus
Higher-Order Strictness Analysis in Untyped λ Calculus (PH, JY), pp. 97–109.
CADECADE-1986-Andrews #logic
Connections and Higher-Order Logic (PBA), pp. 1–4.
ICLPICLP-1986-MillerN86 #logic programming
Higher-Order Logic Programming (DM, GN), pp. 448–462.
LICSLICS-1986-AmadioBL #equation #λ-calculus
The Finitary Projection Model for Second Order λ Calculus and Solutions to Higher Order Domain Equations (RMA, KBB, GL), pp. 122–130.
LICSLICS-1986-MakowskyS #equivalence #on the #semantics #standard #verification
On the Equivalence of Weak Second Order and Nonstandard Time Semantics For Various Program Verification Systems (JAM, IS), pp. 293–300.
FPCAFPCA-1985-Bellot85 #programming
High Order Programming in Extended FP (PB), pp. 65–80.
FPCAFPCA-1985-Sheeran85 #architecture #array #design #using
Designing Regular Array Architectures using Higher Order Functions (MS), pp. 220–237.
CADECADE-1984-Simon #algorithm #linear
A Linear Time Algorithm for a Subcase of Second Order Instantiation (DS), pp. 209–223.
STOCSTOC-1981-MullerS #automaton #graph #logic #problem #reachability
Pushdown Automata, Graphs, Ends, Second-Order Logic, and Reachability Problems (DEM, PES), pp. 46–54.
ICSEICSE-1978-Fisher #design #interactive #requirements
The Interaction Between the Preliminary Designs and the Technical Requirements for the DoD Common High Order Language (DAF), pp. 82–83.
STOCSTOC-1974-Robertson #complexity #monad
Structure of Complexity in the Weak Monadic Second-Order Theories of the Natural Numbers (ELR), pp. 161–171.
STOCSTOC-1970-Manna
Second-Order Mathematical Theory of Computation (ZM), pp. 158–168.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.