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